proposition: Lemma eq_suml_odds n : suml (odds n) = n ^ 2.
proof: Proof. elim: n => //= n IHn; rewrite suml_cons. rewrite suml_add2list IHn addnCA addnA. by rewrite -(addn1 n) sqrnD size_odds muln1. Qed.
imports: mathcomp(all_ssreflect)