proposition: Lemma binop_assoc (n m p: T): binop n (binop m p) == binop (binop n m) p.
proof: Proof. Proof with auto. unfold eq, le. simpl. split; intros. apply BinopBound_sym. apply BinopBound_assoc. apply BinopBound_sym. apply BinopBound_assoc. apply BinopBound_sym... apply BinopBound_le with q... apply BinopBound_assoc. apply BinopBound_le with q... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program