fact: Definition from_parttuple t := rem_trail0 [seq nth 0 t i.+1 - nth 0 t i | i <- iota 0 d].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype