The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Rewrite your goal as forall k n m, k = n+m -> P k

and proceed by inducxtion on k (might work)

but any predicate Q k n m st k = n+m -> Q k n m 

will do (if the induction hypothesis is too weak)

Dominique

---

De: "Kevin Sullivan" <sullivan.kevinj AT gmail.com>
À: coq-club AT inria.fr
Envoyé: Samedi 28 Octobre 2017 07:00:44
Objet: [Coq-Club] Detail regarding induction

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?