proposition: Lemma iota_ltn a b : b <= a -> [seq i <- iota 0 a | i < b] = iota 0 b.
proof: Proof. move=> Hab. rewrite -(subnKC Hab) iotaD add0n filter_cat. rewrite -[RHS]cats0; congr (_ ++ _). - rewrite (eq_in_filter (a2 := predT)) ?filter_predT //. by move=> i /=; rewrite mem_iota add0n /= => ->. - rewrite (eq_in_filter (a2 := pred0)) ?filter_pred0 //. move=> i /=; rewrite mem_iota (subnKC Hab) => /andP[]. by rewrite leqNgt => /negbTE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)