proposition: Lemma comparable_minA : min x (min y z) = min (min x 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) => [xy|xy|xy|<-] [xz|xz|xz|<-]// []//= yz. - by have := lt_trans xy (lt_trans yz xz); rewrite ltxx. - by have := lt_trans xy (lt_trans xz yz); rewrite ltxx. - by have := lt_trans xy xz; rewrite yz ltxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)