proposition: Lemma sumn_incr_nth s i : sumn (incr_nth s i) = (sumn s).+1.
proof: Proof. elim: i s => [/= | i IHi]; first by case=> [| s0 s]. case=> [/= | s0 s /=]; first by rewrite /sumn add0n; elim i. by rewrite (IHi s) addnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype