proposition: Lemma in_part_is_part sh : (forall r c j k, j <= r -> k <= c -> in_shape sh (r, c) -> in_shape sh (j, k)) -> last 1 sh != 0 -> is_part sh.
proof: Proof. rewrite /in_shape => H Hlast. apply/is_partP; split => [|i]; first exact: Hlast. case Hnth : (nth 0 sh i.+1) => [//|n]. apply: (H i.+1 n i n (leqnSn i) (leqnn n)). by rewrite Hnth. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype