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