proposition: Lemma oddsE n : odds n = [seq 2 * i + 1 | i <- iota 0 n].
proof: Proof. rewrite /odds; set k := (0 as X in iota X _). rewrite -[1 in LHS]/(2 * k + 1). elim: n k => //= n IHn k; rewrite {}IHn; congr (_ :: _). by elim: n k => // n IHn k /=; rewrite IHn !mulnS. Qed.
imports: mathcomp(all_ssreflect)