proposition: Lemma Fp_exprnDn n (p1 p2 : {poly 'F_p}) : (p1 + p2) ^+ (p ^ n) = p1 ^+ (p ^ n) + p2 ^+ (p ^ n).
proof: Proof. by elim: n => // n IH; rewrite expnS mulnC !exprM IH Fp_exprnD. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra)