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