proposition: Lemma peano_induction : forall (P:nat->Prop), (forall n, (forall m, m < n -> P m) -> P n) -> (forall n, P n).
proof: Proof. Proof using. introv H. cuts* K: (forall n m, m < n -> P m). nat_comp_to_peano. induction n; introv Le. inversion Le. apply H. intros. apply IHn. nat_math. Qed.
imports: Coq.Arith.Arith Coq.micromega.Lia TLC(LibTactics LibReflect LibBool LibOperation LibRelation LibOrder)