fact: Fixpoint decr_nth v i {struct i} := if v is n :: v' then if i is i'.+1 then n :: decr_nth v' i' else if n is n'.+1 then if n' is _.+1 then n' :: v' else [::] else [::] else [::].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype