coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Kevin Sullivan <sullivan.kevinj AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Detail regarding induction
Date: Sat, 28 Oct 2017 01:00:44 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sullivan.kevinj AT gmail.com; spf=Pass smtp.mailfrom=sullivan.kevinj AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f43.google.com
Ironport-phdr: 9a23:fwNYLxNQwQk1v8VYbQol6mtUPXoX/o7sNwtQ0KIMzox0K/T+rarrMEGX3/hxlliBBdydsK0UzbeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6a8TWO6mtYERLmcAFxO+7dG4jIjs3x2fr4s8nYZBwNjz6ga5tzKg+3pEPfrJ9Fr5FlL/MSxwXIpDNzZuBSxH1hIxrHhAv44sau9Zgl8ClOuvQj38FFWKT+Oa8/SOoLX3wdL2kp6Ziz5lH4RgyV6y5EXw==

Why is it that when one does "induction (n + m)", the context for the first subgoal (where n + m = 0) does not contain n + m = 0 as an assumption?

[Coq-Club] Detail regarding induction, Kevin Sullivan, 10/28/2017
- Re: [Coq-Club] Detail regarding induction, Dominique Larchey-Wendling, 10/28/2017