proposition: Theorem order_induction : A z -> (forall n, z <= n -> A n -> A (S n)) -> (forall n, n < z -> A (S n) -> A n) -> forall n, A n.
proof: Proof. intros Az RS LS n. destruct (lt_trichotomy n z) as [H | [H | H]]. - now apply left_induction; [| | apply lt_le_incl]. - now rewrite H. - now apply right_induction; [| | apply lt_le_incl]. Qed.
imports: NZAxioms NZBase Decidable OrdersTac