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