proposition: Lemma binop_assoc (x y z: T): binop x (binop y z) == binop (binop x y) z.
proof: Proof. unfold eq. simpl. apply o_assoc. Qed.
imports: CoRN.model.totalorder.QposMinMax Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax