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