proposition: Lemma CRmorph_INR : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (n : nat), CRmorph f (INR n) == INR n.
proof: Proof. induction n. - apply CRmorph_rat. - simpl. unfold INR. rewrite (CRmorph_proper f _ (1 + CR_of_Q R1 (Z.of_nat n # 1))). + rewrite CRmorph_plus. unfold INR in IHn. rewrite IHn. rewrite CRmorph_one, <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r. rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. reflexivity. + rewrite <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r. rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits