proposition: Lemma included_conj_partE inner outer : is_part inner -> is_part outer -> included inner outer = included (conj_part inner) (conj_part outer).
proof: Proof. move=> Hinn Hout; apply/idP/idP; first exact: included_conj_part. rewrite -{2}(conj_partK Hinn) -{2}(conj_partK Hout). by apply: included_conj_part; exact: is_part_conj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype