proposition: Lemma sqrnD m n : (m + n) ^ 2 = m ^ 2 + n ^ 2 + 2 * (m * n).
proof: Proof. rewrite -!mulnn mul2n mulnDr !mulnDl (mulnC n) -!addnA. by congr (_ + _); rewrite addnA addnn addnC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring