proposition: Lemma Rrepr_le : forall x y:R, (x <= y)%R <-> Rrepr x <= Rrepr y.
proof: Proof. split. - intros [H|H] abs. + rewrite RbaseSymbolsImpl.Rlt_def in H. apply CRealLtEpsilon in H. exact (CRealLt_asym (Rrepr x) (Rrepr y) H abs). + destruct H. exact (CRealLt_asym (Rrepr x) (Rrepr x) abs abs). - intros. destruct (total_order_T x y). + destruct s. * left. exact r. * right. exact e. + rewrite RbaseSymbolsImpl.Rlt_def in r. apply CRealLtEpsilon in r. contradiction. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions