fact: Fixpoint diff_shape inner outer := if inner is inn0 :: inn then if outer is out0 :: out then out0 - inn0 :: diff_shape inn out else [::] else outer.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype