proposition: Lemma Qmax4_Qlt_upper_bound:forall p q1 q2 q3 q4, p<q1 -> p<q2 -> p<q3 -> p<q4 -> p < Qmax4 q1 q2 q3 q4.
proof: Proof. intros p q1 q2 q3 q4 H1 H2 H3 H4; unfold Qmax4; repeat apply Qmax_Qlt_upper_bound; assumption. Qed.