proposition: Theorem order_induction' : A z -> (forall n, z <= n -> A n -> A (S n)) -> (forall n, n <= z -> A n -> A (P n)) -> forall n, A n.
proof: Proof. intros Az AS AP n; apply order_induction; try assumption. intros m H1 H2. apply AP in H2; [|now apply le_succ_l]. now rewrite pred_succ in H2. Qed.
imports: NZAxioms NZBase Decidable OrdersTac