proposition: Lemma CRmorph_mult_inv : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x : CRcarrier R1) (p : positive), CRmorph f (CRmult R1 x (CR_of_Q R1 (1 # p))) == CRmult R2 (CRmorph f x) (CR_of_Q R2 (1 # p)).
proof: Proof. intros. apply (CRmult_eq_reg_r (CR_of_Q R2 (Z.pos p # 1))). - left. apply (CRle_lt_trans _ (CR_of_Q R2 0)). 1:apply CRle_refl. apply CR_of_Q_lt. reflexivity. - apply (CReq_trans _ (CRmorph f x)). 1:apply (CReq_trans _ (CRmorph f (CRmult R1 (CRmult R1 x (CR_of_Q R1 (1 # p))) (CR_of_Q R1 (Z.pos p # 1))))). { apply CReq_sym, CRmorph_mult_int. } + apply CRmorph_proper. apply (CReq_trans _ (CRmult R1 x (CRmult R1 (CR_of_Q R1 (1 # p)) (CR_of_Q R1 (Z.pos p # 1))))). * destruct (CRisRing R1). apply CReq_sym, Rmul_assoc. * apply (CReq_trans _ (CRmult R1 x 1)). { apply (Rmul_ext (CRisRingExt R1)). 1:apply CReq_refl. apply (CReq_trans _ (CR_of_Q R1 ((1#p) * (Z.pos p # 1)))). { apply CReq_sym, CR_of_Q_mult. } apply (CReq_trans _ (CR_of_Q R1 1)). 2:reflexivity. apply CR_of_Q_morph. reflexivity. } apply CRmult_1_r. + apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRmult R2 (CR_of_Q R2 (1 # p)) (CR_of_Q R2 (Z.pos p # 1))))). 2: apply (Rmul_assoc (CRisRing R2)). apply (CReq_trans _ (CRmult R2 (CRmorph f x) 1)). { apply CReq_sym, CRmult_1_r. } apply (Rmul_ext (CRisRingExt R2)). * apply CReq_refl. * apply (CReq_trans _ (CR_of_Q R2 1)). -- reflexivity. -- apply (CReq_trans _ (CR_of_Q R2 ((1#p)*(Z.pos p # 1)))). ++ apply CR_of_Q_morph. reflexivity. ++ apply CR_of_Q_mult. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs