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