proposition: Lemma CRmorph_mult_pos : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x : CRcarrier R1) (n : nat), CRmorph f (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))) == CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1)).
proof: Proof. induction n. - simpl. destruct (CRisRingExt R1). apply (CReq_trans _ 0). + apply (CReq_trans _ (CRmorph f 0)). 2: apply CRmorph_zero. apply CRmorph_proper. apply (CReq_trans _ (CRmult R1 x 0)). 2: apply CRmult_0_r. apply Rmul_ext. * apply CReq_refl. * reflexivity. + apply (CReq_trans _ (CRmult R2 (CRmorph f x) 0)). * apply CReq_sym, CRmult_0_r. * destruct (CRisRingExt R2). apply Rmul_ext0. -- apply CReq_refl. -- reflexivity. - destruct (CRisRingExt R1), (CRisRingExt R2). transitivity (CRmorph f (CRplus R1 x (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))))). + apply CRmorph_proper. transitivity (CRmult R1 x (CRplus R1 1 (CR_of_Q R1 (Z.of_nat n # 1)))). * apply Rmul_ext. -- reflexivity. -- transitivity (CR_of_Q R1 (1 + (Z.of_nat n # 1))). ++ apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity. ++ rewrite CR_of_Q_plus. reflexivity. * transitivity (CRplus R1 (CRmult R1 x 1) (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))). -- apply CRmult_plus_distr_l. -- apply Radd_ext. ++ apply CRmult_1_r. ++ reflexivity. + apply (CReq_trans _ (CRplus R2 (CRmorph f x) (CRmorph f (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))))). * apply CRmorph_plus. * apply (CReq_trans _ (CRplus R2 (CRmorph f x) (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))). -- apply Radd_ext0. ++ apply CReq_refl. ++ exact IHn. -- apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRplus R2 1 (CR_of_Q R2 (Z.of_nat n # 1))))). 1:apply (CReq_trans _ (CRplus R2 (CRmult R2 (CRmorph f x) 1) (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))). ++ apply Radd_ext0. 2: apply CReq_refl. apply CReq_sym, CRmult_1_r. ++ apply CReq_sym, CRmult_plus_distr_l. ++ apply Rmul_ext0. ** apply CReq_refl. ** apply (CReq_trans _ (CR_of_Q R2 (1 + (Z.of_nat n # 1)))). 1:apply (CReq_trans _ (CRplus R2 (CR_of_Q R2 1) (CR_of_Q R2 (Z.of_nat n # 1)))). { apply Radd_ext0; reflexivity. } { apply CReq_sym, CR_of_Q_plus. } apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs