proposition: Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n.
proof: Proof. intros Hstep. refine (well_founded_induction (gt_wf z) _ _). intros x IH Hzx. apply Hstep; [trivial|]. intros y ? ?%le_succ_l. apply IH; [split|]; order. Qed.
imports: NZAxioms NZBase Decidable OrdersTac