proposition: Lemma oddsE_aux n k : iter n (fun s : seq nat => 2 * k + 1 :: add2list s) [::] = [seq 2 * i + 1 | i <- iota k n].
proof: Proof. elim: n k => //= n IHn k; rewrite {}IHn; congr (_ :: _). by elim: n k => // n IHn k /=; rewrite IHn !mulnS. Qed.
imports: mathcomp(all_ssreflect)