proposition: Lemma CReal_le_lt_trans : forall x y z : CReal, x <= y -> y < z -> x < z.
proof: Proof. intros x y z Hle Hlt. destruct (linear_order_T y x z Hlt) as [Hyltx|Hxltz]. - contradiction. - exact Hxltz. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra