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