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