proposition: Lemma last_incr_nth_non0 sh i : last 1 sh != 0 -> last 1 (incr_nth sh i) != 0.
proof: Proof. rewrite -!nth_last size_incr_nth. case (ltnP i (size sh)) => Hi. - have Hsz : (size sh).-1 < size sh by move: Hi; case: (size sh). rewrite (set_nth_default 0 1 (s := incr_nth _ _)); last by rewrite size_incr_nth Hi Hsz. rewrite nth_incr_nth; apply contra. rewrite addn_eq0 => /andP[_ H]. by rewrite (set_nth_default 0 1). - move=> _; rewrite /= (set_nth_default 0 1). + by rewrite nth_incr_nth eq_refl. + by rewrite size_incr_nth [i < size sh]ltnNge Hi /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype