proposition: Lemma nring_leEq : forall (OF : COrdField) m n, m <= n -> nring (R:=OF) m [<=] nring (R:=OF) n.
proof: Proof. intros. induction m as [| m Hrecm]. simpl in |- *. case n. simpl in |- *. apply leEq_reflexive. intro. apply less_leEq. apply pos_nring_S. case (le_lt_eq_dec (S m) n H). intro. apply less_leEq. apply nring_less. assumption. intro. rewrite e. apply leEq_reflexive. Qed.
imports: CoRN.model.reals.Cauchy_IR CoRN.model.monoids.Nmonoid CoRN.model.rings.Zring CoRN.algebra.CRing_Homomorphisms CoRN.algebra.Expon Coq.QArith.Qpower CoRN.tactics.CornTac