proposition: Lemma Fp_exprnD (p1 p2 : {poly 'F_p}) : (p1 + p2) ^+ p = p1 ^+ p + p2 ^+ p.
proof: Proof. rewrite -[X in _ ^+ X](prednK (prime_gt0 Pp)). rewrite exprDn big_ord_recl /= subn0 mulr1 bin0 mulr1n. rewrite big_ord_recr /bump add1n //= prednK // ?prime_gt0 //; congr (_ + _). rewrite subnn binn mul1r mulr1n big1 ?add0r // => i _. have /dvdnP[k ->] : (p %| 'C(p, (0 <= i) + i))%N. apply: prime_dvd_bin Pp _ => //. by rewrite add1n andTb -[X in (_ < X)%N](prednK (prime_gt0 Pp)) ltnS. by rewrite mulrnA -mulr_natr -polyC1 -polyCMn char_Fp_0 // polyC0 !mulr0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra)