proposition: Lemma BinopBound_sym x y: pred_eq (BinopBound x y) (BinopBound y x).
proof: Proof. Proof with auto. split; intros [a b xa yb r E]. apply (is_binop_bound y x b a yb xa). rewrite o_comm... apply (is_binop_bound x y b a yb xa). rewrite o_comm... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program