proposition: Lemma included_behead p1 p2 : included p1 p2 -> included (behead p1) (behead p2).
proof: Proof. by case: p1 => //= a l; case: p2 => //= b s /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype