I stand corrected, I didn’t realize strong induction was well-founded
induction on lt (this is actually the first I’ve seen a reference to
[well_founded induction lt_wf]).
Indeed you could have proved your strong_induction that way ...
Definition strong_induction := well_founded_induction lt_wf.
Notice you also have recursion principles (to build terms in Set/Type
instead of just prove formulas in Prop)
and a fixpoint based on well-founded induction
if you want to define terms with which you need to compute.
In that case, it would be good to find a place in the documentation to
mention this, such that searching for “strong induction coq” pulls this up.
A good place to start with is in the documentation of the
Standard Library module Wf.
Well founded induction is a really tremendous tool to prove
by induction in Coq. Do not hesitate to define lots of different
induction principles to suit your needs.