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