proposition: Lemma Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1.
proof: Proof. intros. intro abs. rewrite RbaseSymbolsImpl.Rlt_def in H, abs. apply CRealLtEpsilon in H. apply CRealLtEpsilon in abs. apply (CRealLt_asym (Rrepr r1) (Rrepr r2)); assumption. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions