proposition: Lemma subr_sqrDB x y : (x + y) ^+ 2 - (x - y) ^+ 2 = x * y *+ 4.
proof: Proof. rewrite sqrrD sqrrB -!(addrAC _ (y ^+ 2)) opprB. by rewrite addrC addrA subrK -mulrnDr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)