proposition: Lemma IR_pring_as_CR : forall p, (IRasCR (pring _ p) == @pring CRasCRing p)%CR.
proof: Proof. unfold pring. intro p. simpl. cut (IRasCR [1] == 1)%CR;[|apply IR_One_as_CR]. generalize ([1]:IR). generalize (1%CR). induction p;intros a b Hab. - simpl. assert (IRasCR (([0][+][1][+][1])[*]b) == (0+1+1)*a)%CR as H. { simpl. rewrite -> IR_mult_as_CR. repeat rewrite -> IR_plus_as_CR. repeat rewrite -> IR_One_as_CR. rewrite -> IR_Zero_as_CR. rewrite -> Hab. reflexivity. } pose proof (IHp _ _ H) as X. simpl in X. set (c:=pring_aux CRasCRing p ((0 + 1 + 1) * a)%CR) in *. clearbody c. rewrite <- X. rewrite -> IR_plus_as_CR. rewrite -> Hab. reflexivity. - simpl. assert (IRasCR (([0][+][1][+][1])[*]b)== (0+1+1)*a)%CR. simpl. rewrite -> IR_mult_as_CR. repeat rewrite -> IR_plus_as_CR. repeat rewrite -> IR_One_as_CR. simpl. rewrite -> IR_Zero_as_CR. simpl. rewrite -> Hab. reflexivity. apply (IHp _ _ H). - simpl. assumption. 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