proposition: Lemma max_min_distr n m p : max n (min m p) == min (max n m) (max n p).
proof: Proof. symmetry. apply min_mono. - eauto with *. - repeat red; intros. apply max_le_compat_l; auto. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics