proposition: Lemma CRealLtForget : forall x y : CReal, x < y -> CRealLtProp x y.
proof: Proof. intros. destruct H. exists x0. exact q. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra