proposition: Lemma Qmax4_informative:forall q1 q2 q3 q4, {Qmax4 q1 q2 q3 q4=q1} + {Qmax4 q1 q2 q3 q4=q2} + {Qmax4 q1 q2 q3 q4=q3} + {Qmax4 q1 q2 q3 q4=q4}.
proof: Proof. intros q1 q2 q3 q4; unfold Qmax4; destruct (Qmax_or_informative (Qmax q1 q2) (Qmax q3 q4)) as [H|H]; rewrite H; [ left; left; exact (Qmax_or_informative q1 q2) | destruct (Qmax_or_informative q3 q4) as [H'|H']; rewrite H'; auto]. Qed.