proposition: Lemma Rrepr_IPR2 : forall n : positive, CRealEq (Rrepr (IPR_2 n)) (inject_Z (Z.pos (n~0))).
proof: Proof. induction n. - simpl. replace (Z.pos n~1~0) with ((Z.pos n~0 + 1) + (Z.pos n~0 + 1))%Z. + rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, inject_Z_plus, inject_Z_plus. rewrite Rrepr_plus, Rrepr_plus, <- IHn. rewrite Rquot2, CReal_mult_plus_distr_r, CReal_mult_1_l. rewrite (CReal_plus_comm 1%CReal). repeat rewrite CReal_plus_assoc. apply CReal_plus_morph. * reflexivity. * reflexivity. + repeat rewrite <- Pos2Z.inj_add. apply f_equal. rewrite Pos.add_diag. apply f_equal. rewrite Pos.add_1_r. reflexivity. - simpl. replace (Z.pos n~0~0) with ((Z.pos n~0) + (Z.pos n~0))%Z. + rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, inject_Z_plus. rewrite Rrepr_plus, <- IHn. rewrite Rquot2, CReal_mult_plus_distr_r, CReal_mult_1_l. reflexivity. + rewrite <- Pos2Z.inj_add. apply f_equal. rewrite Pos.add_diag. reflexivity. - simpl. rewrite Rrepr_plus, RbaseSymbolsImpl.R1_def, Rquot2. replace 2%Z with (1 + 1)%Z. + rewrite inject_Z_plus. reflexivity. + reflexivity. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions