proposition: Lemma wf_peano_lt : wf Peano.lt.
proof: Proof. Proof using. intros x. induction x using peano_induction. apply~ Acc_intro. intros. applys H. math. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)