fact: Definition outer_shape inner size_seq := [seq p.1 + p.2 | p <- zip (pad 0 (size (size_seq)) inner) size_seq].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype