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