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