proposition: Lemma comparable_min_maxr x y z : x >=< y -> x >=< z -> y >=< z -> min x (max y z) = max (min x y) (min x z).
proof: Proof. move=> xy xz yz; rewrite ![min x _]comparable_minC// ?comparable_maxr//. by rewrite comparable_min_maxl// 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)