proposition: Lemma max_le_compat n m p q : n <= m -> p <= q -> max n p <= max m q.
proof: Proof. intros Hnm Hpq. assert (LE := max_le_compat_l _ _ m Hpq). assert (LE' := max_le_compat_r _ _ p Hnm). order. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics