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