proposition: Lemma max_min_absorption n m : min n (max n m) == n.
proof: Proof. intros. destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E. - destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order. - apply min_l; auto. order. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics