proposition: Theorem order_induction_0 : A 0 -> (forall n, 0 <= n -> A n -> A (S n)) -> (forall n, n < 0 -> A (S n) -> A n) -> forall n, A n.
proof: Proof. Proof (order_induction 0). Theorem order_induction'_0 : A 0 -> (forall n, 0 <= n -> A n -> A (S n)) -> (forall n, n <= 0 -> A n -> A (P n)) -> forall n, A n. Proof (order_induction' 0). Theorem lt_ind : forall (n : t), A (S n) -> (forall m, n < m -> A m -> A (S m)) -> forall m, n < m -> A m. Proof. intros n H1 H2 m H3. apply right_induction with (S n); [assumption | | now apply le_succ_l]. intros; apply H2; try assumption. now apply le_succ_l. Qed.
imports: NZAxioms NZBase Decidable OrdersTac