proposition: Lemma sqrn_dist n1 n2 : `|n1 - n2| ^ 2 + 2 * (n1 * n2) = n1 ^ 2 + n2 ^ 2.
proof: Proof. wlog le_n21: n1 n2 / n2 <= n1. move=> IH; case/orP: (leq_total n2 n1) => /IH //. by rewrite (addnC (n2 ^ 2)) (mulnC n2) distnC. by rewrite distnEl ?sqrnB ?subnK ?nat_Cauchy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)