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