proposition: Lemma CRmorph_mult_rat : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x : CRcarrier R1) (q : Q), CRmorph f (CRmult R1 x (CR_of_Q R1 q)) == CRmult R2 (CRmorph f x) (CR_of_Q R2 q).
proof: Proof. intros. destruct q as [a b]. apply (CReq_trans _ (CRmult R2 (CRmorph f (CRmult R1 x (CR_of_Q R1 (a # 1)))) (CR_of_Q R2 (1 # b)))). - apply (CReq_trans _ (CRmorph f (CRmult R1 (CRmult R1 x (CR_of_Q R1 (a # 1))) (CR_of_Q R1 (1 # b))))). 2: apply CRmorph_mult_inv. apply CRmorph_proper. apply (CReq_trans _ (CRmult R1 x (CRmult R1 (CR_of_Q R1 (a # 1)) (CR_of_Q R1 (1 # b))))). { apply (Rmul_ext (CRisRingExt R1)). { apply CReq_refl. } apply (CReq_trans _ (CR_of_Q R1 ((a#1)*(1#b)))). - apply CR_of_Q_morph. unfold Qeq; simpl. rewrite Z.mul_1_r. reflexivity. - apply CR_of_Q_mult. } apply (Rmul_assoc (CRisRing R1)). - apply (CReq_trans _ (CRmult R2 (CRmult R2 (CRmorph f x) (CR_of_Q R2 (a # 1))) (CR_of_Q R2 (1 # b)))). { apply (Rmul_ext (CRisRingExt R2)). { apply CRmorph_mult_int. } apply CReq_refl. } apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRmult R2 (CR_of_Q R2 (a # 1)) (CR_of_Q R2 (1 # b))))). { apply CReq_sym, (Rmul_assoc (CRisRing R2)). } apply (Rmul_ext (CRisRingExt R2)). { apply CReq_refl. } apply (CReq_trans _ (CR_of_Q R2 ((a#1)*(1#b)))). { apply CReq_sym, CR_of_Q_mult. } apply CR_of_Q_morph. unfold Qeq; simpl. rewrite Z.mul_1_r. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs