proposition: Lemma comparable_maxACA x y z t : x >=< y -> x >=< z -> x >=< t -> y >=< z -> y >=< t -> z >=< t -> max (max x y) (max z t) = max (max x z) (max y t).
proof: Proof. move=> xy xz xt yz yt zt; rewrite comparable_maxA// ?comparable_maxl//. rewrite [max _ z]comparable_maxAC// -comparable_maxA// ?comparable_maxl//. by rewrite inE 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)