proposition: Lemma CReal_lt_trans : forall x y z : CReal, x < y -> y < z -> x < z.
proof: Proof. intros x y z Hxlty Hyltz. apply (CReal_lt_le_trans _ y _ Hxlty). apply CRealLt_asym; exact Hyltz. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra