proposition: Lemma filter_iota_leq n m j : j < n -> [seq i <- iota m n | i <= m + j] = iota m j.+1.
proof: Proof. elim: n m j => [//|n IHn] m [|j] jlen /=; rewrite leq_addr. rewrite (@eq_in_filter _ _ pred0) ?filter_pred0// => i. by rewrite addn0 leqNgt mem_iota => /andP[->]. by rewrite addnS -addSn IHn -1?ltnS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)