proposition: Lemma Rrepr_appart_0 : forall x:R, (x < R0 \/ R0 < x) -> CReal_appart (Rrepr x) (inject_Q 0).
proof: Proof. intros. apply CRealLtDisjunctEpsilon. destruct H. - left. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H. exact H. - right. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H. exact H. Qed.
imports: ZArith_base QArith_base ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ClassicalDedekindReals