proposition: Lemma comparable_minACA x y z t : x >=< y -> x >=< z -> x >=< t -> y >=< z -> y >=< t -> z >=< t -> min (min x y) (min z t) = min (min x z) (min y t).
proof: Proof. move=> xy xz xt yz yt zt; rewrite comparable_minA// ?comparable_minl//. rewrite [min _ z]comparable_minAC// -comparable_minA// ?comparable_minl//. 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)