Strong natural induction should be simpler #22
Description
I'm a teacher trying to see how far coq is to being usable (and hoping to improve the situation) ; anytime I have a so-called strong induction, I find I always use the same line to get around it, so it's easy to just take it in Ltac and be done:
Ltac strong_nat_induction n := elim: n {-2}n (leqnn n).
makes it possible to do something like:
strong_nat_induction n => [|n IHn].
in proof scripts, and that looks much easier for students.
(NB: I have seen issue rocq-prover/rocq#5343, but what I'm asking is more in terms of usability than in terms of feature.)