Strong natural induction should be simpler

[SnarkBoojum]

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 coq/coq#5343, but what I'm asking is more in terms of usability than in terms of feature.)