proposition: Lemma includedP inner outer : reflect (size inner <= size outer /\ forall i, nth 0 inner i <= nth 0 outer i) (included inner outer).
proof: Proof. apply (iffP idP). - elim: inner outer => [// | inn0 inn IHinn] /=. by move=> outer _; split; last by move=> i; rewrite nth_nil. case=> [//= | out0 out] /= /andP[H0 {}/IHinn [Hsize H]]. split; first by rewrite ltnS. by case. - elim: inner outer => [// | inn0 inn IHinn] /=. case=> [ [] // | out0 out] [] /=. rewrite ltnS => Hsize H. apply/andP; split; first exact: (H 0). apply: IHinn; split; first exact: Hsize. by move=> i; exact: (H i.+1). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype