proposition: Lemma Rrepr_IPR : forall n : positive, CRealEq (Rrepr (IPR n)) (inject_Z (Z.pos n)).
proof: Proof. intro n. destruct n. - unfold IPR. rewrite Rrepr_plus. replace (n~1)%positive with (n~0 + 1)%positive. + rewrite Pos2Z.inj_add, inject_Z_plus, <- Rrepr_IPR2, CReal_plus_comm. rewrite RbaseSymbolsImpl.R1_def, Rquot2. reflexivity. + rewrite Pos.add_1_r. reflexivity. - apply Rrepr_IPR2. - unfold IPR. rewrite RbaseSymbolsImpl.R1_def. apply Rquot2. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions