proposition: Lemma nth_decr_nth sh i : nth 0 (decr_nth sh i) i = (nth 0 sh i).-1.
proof: Proof. by elim: i sh => [| i IHi] [| [|[|s0]] sh] /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype