proposition: Lemma subr_sqr x y : x ^+ 2 - y ^+ 2 = (x - y) * (x + y).
proof: Proof. by rewrite subrXX !big_ord_recr big_ord0 /= add0r mulr1 mul1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)