proposition: Lemma max_assoc m n p : max m (max n p) == max (max m n) p.
proof: Proof. destruct (max_spec n p) as [(H,E)|(H,E)]; rewrite E; destruct (max_spec m n) as [(H',E')|(H',E')]; rewrite E', ?E; try easy. - apply max_r; order. - symmetry. apply max_l; order. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics