proposition: Theorem strong_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 strong_right_induction. + assumption. + now apply lt_le_incl. Qed.
imports: NZAxioms NZBase Decidable OrdersTac