proposition: Lemma min_comm: forall x y, min x y == min y x.
proof: Proof. intros. destruct x,y. unfold eq. simpl. apply Q.min_comm. Qed.
imports: CoRN.model.totalorder.QposMinMax Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax