proposition: Lemma IR_inj_Q_as_CR : forall (a:Q), (IRasCR (inj_Q IR a)==('a))%CR.
proof: Proof. intros [n d]. unfold inj_Q. rewrite -> IR_div_as_CR_1. generalize (map_pres_ap_zero IR CRasCReals (iso_map_rht CRasCReals IR CRIR_iso) (nring (R:=IR) (nat_of_P d)) (den_is_nonzero IR (n # d)%Q)). intros d_. setoid_replace (n#d)%Q with ((n # 1) * / (d # 1))%Q by (unfold Qeq; simpl; rewrite Z.mul_1_r; reflexivity). rewrite <- CRmult_Qmult. assert (d__:('d >< 0)%CR). { apply Qap_CRap. discriminate. } rewrite <- (CRinv_Qinv d d__). unfold cf_div. assert (X:(forall (n:positive), IRasCR (nring (R:=IR) (nat_of_P n)) == ' Zpos n)%CR). { intros x. clear -x. rewrite <- convert_is_POS. induction (nat_of_P x); clear x. apply IR_Zero_as_CR. simpl. rewrite -> IR_plus_as_CR. rewrite -> IHn. rewrite -> IR_One_as_CR. simpl. rewrite -> CRplus_Qplus. rewrite -> CReq_Qeq. unfold Qeq. simpl. rewrite Pmult_1_r. rewrite <- POS_anti_convert. ring_simplify. symmetry. rewrite Zplus_comm. apply (inj_plus 1 n). } apply (mult_wd CRasCRing);[|apply: f_rcpcl_wd;apply (X d)]. destruct n as [|p|p];[apply IR_Zero_as_CR| |];simpl. transitivity (IRasCR (nring (nat_of_P p))). apply IRasCR_wd. apply pring_convert. apply (X p). transitivity (IRasCR [--](nring (nat_of_P p))). apply IRasCR_wd. apply csf_wd_unfolded. apply pring_convert. rewrite -> IR_opp_as_CR. rewrite -> X. rewrite -> CRopp_Qopp. 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