proposition: Lemma min_assoc m n p : min m (min n p) == min (min m n) p.
proof: Proof. destruct (min_spec n p) as [(H,E)|(H,E)]; rewrite E; destruct (min_spec m n) as [(H',E')|(H',E')]; rewrite E', ?E; try easy. - symmetry. apply min_l; order. - apply min_r; order. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics