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