proposition: Lemma delta_square n : (8 * delta n).+1 = n.*2.+1 ^ 2.
proof: Proof. elim: n => // n IH. rewrite deltaS mulnDr -addSn IH. rewrite doubleS -addn1 -addnS -addSn addn1. rewrite sqrnD -addnA /=. congr (_ + _). rewrite mulnS. rewrite [_ * 2]mulSn mulnDr addnA. congr (_ + _). by rewrite mulnCA -muln2 -!mulnA mulnC. Qed.
imports: mathcomp(all_ssreflect)