fact: Definition parttuple_minn sh1 sh2 := [tuple minn (tnth (parttuple sh1) i) (tnth (parttuple sh2) i) | i < d.+1].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype