proposition: Lemma ing_nring' : forall m n : nat, CS_seq _ (nring (R:=R_COrdField') n) m [=] CS_seq _ (inject_Q (nring n)) m.
proof: Proof. intros. induction n as [| n Hrecn]; simpl in |- *; algebra. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals