proposition: Lemma comparable_maxCA x y z : x >=< y -> x >=< z -> y >=< z -> max x (max y z) = max y (max x z).
proof: Proof. move=> xy xz yz; rewrite comparable_maxA// [max x y]comparable_maxC//. by rewrite -comparable_maxA// 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)