proposition: Lemma Rrepr_IZR : forall n : Z, CRealEq (Rrepr (IZR n)) (inject_Z n).
proof: Proof. intros [|p|n]. - unfold IZR. rewrite RbaseSymbolsImpl.R0_def. apply Rquot2. - apply Rrepr_IPR. - unfold IZR. rewrite Rrepr_opp, Rrepr_IPR. rewrite <- opp_inject_Z. replace (- Z.pos n)%Z with (Z.neg n); reflexivity. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions