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