proposition: Lemma CReal_le_trans : forall x y z : CReal, x <= y -> y <= z -> x <= z.
proof: Proof. intros x y z Hxley Hylez contra. apply Hylez. apply (CReal_lt_le_trans _ x); assumption. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra