proposition: Lemma Rrepr_appart : forall x y:R, (x <> y)%R -> Rrepr x # Rrepr y.
proof: Proof. intros. destruct (total_order_T x y). - destruct s. + left. rewrite RbaseSymbolsImpl.Rlt_def in r. apply CRealLtEpsilon. exact r. + contradiction. - right. rewrite RbaseSymbolsImpl.Rlt_def in r. apply CRealLtEpsilon. exact r. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions