proposition: Lemma outer_shape_pad0 inner sz : outer_shape (pad 0 (size sz) inner) sz = outer_shape inner sz.
proof: Proof. rewrite /outer_shape; congr map; congr zip. rewrite /= size_cat size_nseq. set n := (X in (_++ _) ++ nseq X _). suff -> : n = 0 by rewrite /= cats0. rewrite {}/n. move: (size sz) (size inner) => a b. case: (ltnP a b) => [/ltnW | ] H. - by move: H; rewrite /leq => /eqP H; rewrite H addn0 H. - by rewrite (subnKC H) subnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype