proposition: Theorem le_ind : forall (n : t), A n -> (forall m, n <= m -> A m -> A (S m)) -> forall m, n <= m -> A m.
proof: Proof. intros n H1 H2 m H3. now apply right_induction with n. Qed.
imports: NZAxioms NZBase Decidable OrdersTac