proposition: Lemma included_conj_part inner outer : is_part inner -> is_part outer -> included inner outer -> included (conj_part inner) (conj_part outer).
proof: Proof. move=> Hinn Hout /includedP[Hsz Hincl]. apply/part_includedP => [|i]; first exact: is_part_conj. by rewrite -conj_leqE //; apply (leq_trans (Hincl _)); rewrite conj_leqE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype