proposition: Lemma is_part_subseq sh1 sh2 : subseq sh1 sh2 -> is_part sh2 -> is_part sh1.
proof: Proof. rewrite !is_part_sortedE => Hsub /andP[Hsort H0]. rewrite (subseq_sorted _ Hsub Hsort) //=. by move: H0; apply contra => /(mem_subseq Hsub). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype