proposition: Lemma iota_geq a b : [seq i <- iota 0 a | b <= i] = iota b (a - b).
proof: Proof. elim: a => [//=| n IHn]. rewrite -addn1 iotaD add0n /= filter_cat IHn {IHn} /=. case: leqP => Hb. - by rewrite addn1 (subSn Hb) -addn1 iotaD /= subnKC. - rewrite addn1 cats0. have := Hb; rewrite /leq => /eqP ->. by have := ltnW Hb; rewrite /leq => /eqP ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)