proposition: Lemma CRmorph_mult_int : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x : CRcarrier R1) (n : Z), CRmorph f (CRmult R1 x (CR_of_Q R1 (n # 1))) == CRmult R2 (CRmorph f x) (CR_of_Q R2 (n # 1)).
proof: Proof. intros. destruct (NatOfZ n) as [p [pos|neg]]. - subst n. apply CRmorph_mult_pos. - subst n. apply (CReq_trans _ (CRopp R2 (CRmorph f (CRmult R1 x (CR_of_Q R1 (Z.of_nat p # 1)))))). + apply (CReq_trans _ (CRmorph f (CRopp R1 (CRmult R1 x (CR_of_Q R1 (Z.of_nat p # 1)))))). 2: apply CRmorph_opp. apply CRmorph_proper. apply (CReq_trans _ (CRmult R1 x (CR_of_Q R1 (- (Z.of_nat p # 1))))). * destruct (CRisRingExt R1). apply Rmul_ext. -- apply CReq_refl. -- apply CR_of_Q_morph. reflexivity. * apply (CReq_trans _ (CRmult R1 x (CRopp R1 (CR_of_Q R1 (Z.of_nat p # 1))))). -- destruct (CRisRingExt R1). apply Rmul_ext. ++ apply CReq_refl. ++ apply CR_of_Q_opp. -- apply CReq_sym, CRopp_mult_distr_r. + apply (CReq_trans _ (CRopp R2 (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat p # 1))))). * destruct (CRisRingExt R2). apply Ropp_ext. apply CRmorph_mult_pos. * apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRopp R2 (CR_of_Q R2 (Z.of_nat p # 1))))). -- apply CRopp_mult_distr_r. -- destruct (CRisRingExt R2). apply Rmul_ext. ++ apply CReq_refl. ++ apply (CReq_trans _ (CR_of_Q R2 (- (Z.of_nat p # 1)))). ** apply CReq_sym, CR_of_Q_opp. ** apply CR_of_Q_morph. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs