proposition: Theorem lt_wf : well_founded Rlt.
proof: Proof. intros a. constructor. revert a. refine (central_induction _ _ z _ _). - solve_proper. - intros y [??]. order. - intros x. split. + intros IH y [? [? | ->]%lt_succ_r%lt_eq_cases]. * now apply IH. * now constructor. + intros IH y [? ?%lt_lt_succ_r]. now apply IH. Qed.
imports: NZAxioms NZBase Decidable OrdersTac