proposition: Lemma comparable_minAC x y z : x >=< y -> x >=< z -> y >=< z -> min (min x y) z = min (min x z) y.
proof: Proof. move=> xy xz yz; rewrite -comparable_minA// [min y z]comparable_minC//. by rewrite comparable_minA// 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)