proposition: Theorem left_induction : A z -> left_step -> forall n, n <= z -> A n.
proof: Proof. intros Az LS; apply strong_left_induction. intros n H1 H2. le_elim H1. - apply LS; trivial. apply H2; [now apply le_succ_l | now apply eq_le_incl]. - rewrite H1; apply Az. Qed.
imports: NZAxioms NZBase Decidable OrdersTac