proposition: Lemma ltn_ind P : (forall n, (forall m, m < n -> P m) -> P n) -> forall n, P n.
proof: Proof. move=> accP M; have [n leMn] := ubnP M; elim: n => // n IHn in M leMn *. by apply/accP=> p /leq_trans/(_ leMn)/IHn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring