proposition: Lemma subrXX_comm x y n (cxy : comm x y) : x ^+ n - y ^+ n = (x - y) * (\sum_(i < n) x ^+ (n.-1 - i) * y ^+ i).
proof: Proof. case: n => [|n]; first by rewrite big_ord0 mulr0 subrr. rewrite mulrBl !big_distrr big_ord_recl big_ord_recr /= subnn mulr1 mul1r. rewrite subn0 -!exprS opprD -!addrA; congr (_ + _); rewrite addrA -sumrB. rewrite big1 ?add0r // => i _; rewrite !mulrA -exprS -subSn ?(valP i) //. by rewrite subSS (commrX _ (commr_sym cxy)) -mulrA -exprS subrr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)