fact: Fixpoint incr_first_n sh n := if sh is s0 :: s then if n is n'.+1 then s0.+1 :: incr_first_n s n' else sh else nseq n 1.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype