proposition: Lemma min_case (P: T -> Type): (forall x y: T, x == y -> P x -> P y) -> forall n m, P n -> P m -> P (min n m).
proof: Proof. Proof with auto. intros. unfold min, binop. generalize (binop_obligation_1 Qmin Qmin_nonneg n m). apply Q.min_case; intros. pose proof q. rewrite <- H in H0. apply X with (exist (Qle 0) x H0)... apply X with n... reflexivity. apply X with m... reflexivity. Qed.
imports: CoRN.model.totalorder.QposMinMax Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax