proposition: Lemma CRealEq_sym : forall x y : CReal, CRealEq x y -> CRealEq y x.
proof: Proof. intros. destruct H. split; intro abs; contradiction. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra