proposition: Lemma comparable_max_minl : max (min x y) z = min (max x z) (max y z).
proof: Proof. move: cmp_xy cmp_xz cmp_yz; rewrite !(fun_if, if_arg)/=. move: (P x y) (P x z) (P y z). move=> [xy|xy|xy|<-] [xz|xz|xz|<-] [yz|yz|yz|//->]//= _; rewrite ?ltxx//. - by have := lt_trans xy (lt_trans yz xz); rewrite ltxx. - by have := lt_trans xy (lt_trans xz yz); rewrite ltxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)