proposition: Lemma max_min_modular n m p : max n (min m (max n p)) == min (max n m) (max n p).
proof: Proof. rewrite <- max_min_distr. destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *. destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'. - rewrite 2 max_l; try order. rewrite min_le_iff; auto. - rewrite 2 max_l; try order. rewrite min_le_iff; auto. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics