proposition: Lemma Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3.
proof: Proof. intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H, H0. apply CRealLtEpsilon in H. apply CRealLtEpsilon in H0. apply CRealLtForget. apply (CReal_lt_trans (Rrepr r1) (Rrepr r2) (Rrepr r3)); assumption. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions