proposition: Lemma sqrnB m n : n <= m -> (m - n) ^ 2 = m ^ 2 + n ^ 2 - 2 * (m * n).
proof: Proof. move/subnK <-; rewrite addnK sqrnD -addnA -addnACA -addnA. by rewrite addnn -mul2n -mulnDr -mulnDl addnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring