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