proposition: Lemma is_part_catl sh1 sh2 : is_part (sh1 ++ sh2) -> is_part sh2.
proof: Proof. exact/is_part_subseq/suffix_subseq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype