proposition: Lemma included_pad0 inner outer : included inner outer = included (pad 0 (size outer) inner) outer.
proof: Proof. elim: inner outer => [| inn0 inn IHinn] /= outer /=. by rewrite subn0; elim: outer. case: outer => // out0 out. by rewrite subSS IHinn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype