fact: Definition cast_intpartn m n (eq_mn : m = n) p := let: erefl in _ = n := eq_mn return 'P_n in p.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype