proposition: Theorem right_induction : A z -> right_step -> forall n, z <= n -> A n.
proof: Proof. intros Az RS; apply strong_right_induction. intros n H1 H2. le_elim H1. - apply lt_exists_pred in H1. destruct H1 as [k [H3 H4]]. rewrite H3. apply RS; trivial. apply H2; trivial. rewrite H3; apply lt_succ_diag_r. - rewrite <- H1; apply Az. Qed.
imports: NZAxioms NZBase Decidable OrdersTac