proposition: Lemma sumn_pred1_iota a b x : sumn [seq ((i == x) : nat) | i <- iota a b] = (a <= x < a + b).
proof: Proof. elim: b a => [/=| b IHb] a. by case: andP => [|//] [/leq_ltn_trans H{}/H]; rewrite addn0 ltnn. rewrite addnS ltnS -add1n iotaD map_cat /= leq_eqVlt addn1 {}IHb addSn ltnS. by case: eqP => [->|_]//=; rewrite ltnn addn0 leq_addr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)