proposition: Lemma part_includedP inner outer : is_part inner -> reflect (forall i, nth 0 inner i <= nth 0 outer i) (included inner outer).
proof: Proof. move=> Hinn; apply (iffP (includedP _ _)) => [[]//|H]; split; last by []. case Hsz : (size inner) => [//|n]. have /(nth_part_non0 Hinn) : n < size inner by rewrite Hsz. rewrite -lt0n => /leq_trans/(_ (H _)). by apply: contraTltn => /(nth_default 0) ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype