proposition: Lemma Qmin_nondecreasing: forall q1 q2 p1 p2, q1 <= p1 -> q2 <= p2 -> Qmin q1 q2 <= Qmin p1 p2.
proof: Proof. intros q1 q2 p1 p2 H1 H2; unfold Qmin; destruct (Q_le_lt_dec q1 q2); destruct (Q_le_lt_dec p1 p2); trivial; [apply Qle_trans with q2| apply Qlt_le_weak; apply Qlt_le_trans with q1]; trivial. Qed.