proposition: Lemma CRmorph_mult : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x y : CRcarrier R1), CRmorph f (CRmult R1 x y) == CRmult R2 (CRmorph f x) (CRmorph f y).
proof: Proof. intros. destruct (CR_archimedean R1 (CRopp R1 y)) as [p pmaj]. apply (CRplus_eq_reg_r (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.pos p # 1)))). apply (CReq_trans _ (CRmorph f (CRmult R1 x (CRplus R1 y (CR_of_Q R1 (Z.pos p # 1)))))). - apply (CReq_trans _ (CRplus R2 (CRmorph f (CRmult R1 x y)) (CRmorph f (CRmult R1 x (CR_of_Q R1 (Z.pos p # 1)))))). + apply (Radd_ext (CRisRingExt R2)). * apply CReq_refl. * apply CReq_sym, CRmorph_mult_int. + apply (CReq_trans _ (CRmorph f (CRplus R1 (CRmult R1 x y) (CRmult R1 x (CR_of_Q R1 (Z.pos p # 1)))))). * apply CReq_sym, CRmorph_plus. * apply CRmorph_proper. apply CReq_sym, CRmult_plus_distr_l. - apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRmorph f (CRplus R1 y (CR_of_Q R1 (Z.pos p # 1)))))). + apply CRmorph_mult_pos_pos. apply (CRplus_lt_compat_l R1 y) in pmaj. apply (CRle_lt_trans _ (CRplus R1 y (CRopp R1 y))). 2: exact pmaj. apply (CRisRing R1). + apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRplus R2 (CRmorph f y) (CR_of_Q R2 (Z.pos p # 1))))). * apply (Rmul_ext (CRisRingExt R2)). -- apply CReq_refl. -- apply (CReq_trans _ (CRplus R2 (CRmorph f y) (CRmorph f (CR_of_Q R1 (Z.pos p # 1))))). ++ apply CRmorph_plus. ++ apply (Radd_ext (CRisRingExt R2)). ** apply CReq_refl. ** apply CRmorph_rat. * apply CRmult_plus_distr_l. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs