proposition: Lemma IR_nring_as_CR : forall (n:nat), (IRasCR (nring n) == @nring CRasCRing n)%CR.
proof: Proof. induction n. apply IR_Zero_as_CR. simpl in *. set (a:= (nring (R:=CRasCRing) n)) in *. clearbody a. rewrite -> IR_plus_as_CR. rewrite -> IHn. rewrite -> IR_One_as_CR. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.CauchySeq CoRN.reals.iso_CReals CoRN.reals.R_morphism CoRN.reals.fast.CRArith CoRN.model.reals.CRreal CoRN.tactics.CornTac