proposition: Lemma ou_eq_sym : forall x y, ou_eq x y -> ou_eq y x.
proof: Proof. intros; apply Qeq_sym; auto. Qed.
imports: Coq.QArith.QArith CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields CoRN.tactics.Qauto CoRN.tactics.CornTac