The Coq mailing list

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

Le 05/12/2016 à 16:30, Tej Chajed a écrit :
> The standard library does not include strong induction. Could it be
> added? A proposed addition is
> at 
> _https://github.com/tchajed/strong-induction/blob/master/StrongInduction.v_.
> Comments welcome, including nitpicks on the comments and pull requests.
> 
> Thanks!
> Tej

It is already included ...

Require Import Arith Wf.

Proof.
  ...
  induction n as [ n IHn ] using (well_founded_induction lt_wf).
  ...
Qed.

Dominique