proposition: Lemma CRealLe_refl : forall x : CReal, x <= x.
proof: Proof. intros. intro abs. pose proof (CRealLt_asym x x abs). contradiction. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra