proposition: Lemma max_comm: forall x y, max x y == max y x.
proof: Proof. Proof binop_comm _ _ Q.max_comm. Lemma plus_assoc: forall x y z, x + (y + z) == (x + y) + z. Proof binop_assoc _ _ Qplus_assoc. Lemma mult_assoc: forall x y z, x * (y * z) == (x * y) * z. Proof binop_assoc _ _ Qmult_assoc. Lemma max_assoc: forall x y z, max x (max y z) == max (max x y) z. Proof binop_assoc _ _ Q.max_assoc. Lemma min_assoc: forall x y z, min x (min y z) == min (min x y) z. Proof binop_assoc _ _ Q.min_assoc. Global Instance: Proper (eq ==> eq ==> eq) plus. Proof. unfold plus. apply _. Qed.
imports: CoRN.model.totalorder.QposMinMax Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax