proposition: Lemma comparable_max_minr x y z : x >=< y -> x >=< z -> y >=< z -> max x (min y z) = min (max x y) (max x z).
proof: Proof. move=> xy xz yz; rewrite ![max x _]comparable_maxC// ?comparable_minr//. by rewrite comparable_max_minl// 1?comparable_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)