proposition: Lemma diff_shapeK inner outer : included inner outer -> outer_shape inner (outer / inner) = outer.
proof: Proof. rewrite /outer_shape. elim: inner outer => [| inn0 inn IHinn] /= outer. rewrite subn0 => _; elim: outer => [// | out0 out /= ->]. by rewrite add0n. case: outer => //= out0 out /= /andP[Hin {}/IHinn ->]. by rewrite addnC subnK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype