proposition: Theorem right_induction' : (forall n, n <= z -> A n) -> right_step -> forall n, A n.
proof: Proof. intros L R n. destruct (lt_trichotomy n z) as [H | [H | H]]. - apply L; now apply lt_le_incl. - apply L; now apply eq_le_incl. - apply right_induction. + apply L; now apply eq_le_incl. + assumption. + now apply lt_le_incl. Qed.
imports: NZAxioms NZBase Decidable OrdersTac