proposition: Lemma sum_odd n : \sum_(0 <= i < n.*2 | odd i) i = n ^ 2.
proof: Proof. elim: n => [|n IHn]; first by rewrite big_geq. rewrite doubleS big_mkcond 2?big_nat_recr // -big_mkcond /=. rewrite {}IHn odd_double /= addn0 -addnn -!mulnn. by rewrite mulSn mulnC mulSn addnA addSn addnC. Qed.
imports: mathcomp(all_ssreflect)