.. coq::

   From mathcomp Require Import all_ssreflect.

   From mathcomp Require Import all_algebra.

.. coq:: no-in

   Notation "'\ccneq{' p '}{' q } " := (p != q).
   Notation "'\cceq{' p '}{' q } " := (p == q).
   Notation "'\ccprimegtz{' p }" := (prime_gt0 p).
   Notation "'\ccpolyX'" := 'X%R.
   Notation "'\ccpolyXn{' n }" := ('X^n)%R.
   Notation "'\ccelem{' l } { n }" := (nth (GRing.zero _) l n).
   Notation "'\ccord{' n }" := (ordinal n).
   Notation "'\ccordz{}'" := ord0.
   Notation "'\ccNat{}'" := nat.
   Notation "'\ccSucc{' n '}'" := (S n).
   Notation "'\ccSucct{' n '}'" := (S (S n)).
   Notation "'\ccpred{' n '}'" := (predn n).
   Infix "\leq" := leq (at level 40).
   Notation "'\ccltn{' n '}{' m }" := (n < m) (at level 40).
   Infix "\times" := muln (at level 40).
   Infix "\rtimes" := GRing.mul (at level 40).
   Notation "\ccbin{ x } { y }" := (binomial x y).
   Notation "\ccPow{ x } { y }" := (expn x y).
   Notation "\ccPowr{ x } { y }" := (GRing.exp x y)
      (at level 29, x at level 29).
   Infix "\times" := muln
     (at level 40).
   Notation "'\ccNsumo{' i '}{' f '}'" :=
     (\sum_i f)
       (format "'\ccNsumo{' i '}{' f '}'", 
       at level 41, f at level 41, i at level 50).
   Notation "'\ccRsumo{' i '}{' f '}'" :=
     (\sum_i f)%R
       (format "'\ccRsumo{' i '}{' f '}'", 
       at level 41, f at level 41, i at level 50).
   Notation "'\ccRsumod{' i '}{' j '}{' k '}{' f '}'" :=
     (\sum_(i | j != k) f)%R
       (format "'\ccRsumod{' i '}{' j '}{' k '}{' f '}'", 
       at level 41, f at level 41, i at level 50).
   Notation "'\ccNsum{' i '}{' r '}{' f '}'" :=
     (\sum_(i < r) f)
       (format "'\ccNsum{' i '}{' r '}{' f '}'", 
       at level 41, f at level 41, i, r at level 50).
   Notation "'\ccRsum{' i '}{' r '}{' f '}'" :=
     (\sum_(i < r) f)%R
       (format "'\ccRsum{' i '}{' r '}{' f '}'", 
       at level 41, f at level 41, i, r at level 50).
   Notation "'\ccNsumd{' i '}{' r '}{' s '}{' f '}'" :=
     (\sum_(r <= i < s) f)
       (format "'\ccNsumd{' i '}{' r '}{' s '}{' f '}'", 
       at level 41, f at level 41, i, r at level 50).
   Notation "'\ccRsumd{' i '}{' r '}{' s '}{' f '}'" :=
     (\sum_(r <= i < s) f)%R
       (format "'\ccRsumd{' i '}{' r '}{' s '}{' f '}'", 
       at level 41, f at level 41, i, r at level 50).
   Notation "'\ccNprod{' i '}{' r '}{' f '}'" :=
     (\prod_(i < r) f)
       (format "'\ccNprod{' i '}{' r '}{' f '}'", 
       at level 41, f at level 41, i, r at level 50).
   Notation "'\ccRprod{' i '}{' r '}{' f '}'" :=
     (\prod_(i < r) f)%R
       (format "'\ccRprod{' i '}{' r '}{' f '}'", 
       at level 41, f at level 41, i, r at level 50).
   Notation "\ccNot{ x }" := (not x) (at level 100).
   Infix "\ccandb" := andb
     (at level 190, right associativity).
   Infix "\wedge" := and
     (at level 190, right associativity).
   Notation "A \Rightarrow{} B" := (forall (_ : A), B)
     (at level 200, right associativity).
   Notation "'\ccForall{' x .. y '}{' P '}'" := (forall x, .. (forall  y, P) ..)
     (at level 200, x binder, y binder, right associativity,
      format "'\ccForall{' x .. y '}{' P '}'").
   Notation "'\ccExists{' x .. y '}{' P '}'" := (exists x, .. (exists  y, P) ..)
     (at level 200, x binder, y binder, right associativity,
      format "'\ccExists{' x .. y '}{' P '}'").
   Notation "'\ccbExists{' x .. y '}{' P '}'" := ([exists x, .. ([exists  y, P]) ..])
     (at level 200, x binder, y binder, right associativity,
      format "'\ccbExists{' x .. y '}{' P '}'").
   Notation " \ccmodn{ a } { b } " := (modn a b)
     (at level 40, a at level 41, b at level 41, left associativity).
   Notation " \ccmodneq{ a } { b } { q }" := (a = b %[mod q]).
   Notation "'\ccdvdn{' a } { b } " := (dvdn a b).
   Notation "'\ccdivn{' a } { b } " := (divn a b).
   Notation "'\ccpoly{' T }" := (poly_of (Phant T)).
   Notation "'\ccprime{' p }" := (prime p).
   Notation "'\ccbump{' p } { q }" := (bump p q).
   Notation "'\cclift{' p } { q }" := (lift p q).
   Notation "'\ccfp{' p }" := ('Z_(pdiv p)).
   Notation "'\ccordinal{' p }" := (Ordinal p).
   Notation "'\ccapp{' f } { p }" := (f p).
   Notation "'\ccffun{' fT }" := (finfun_of (Phant fT)).
   Notation "'\ccdffun{' x } { aT } { E }" := (finfun (fun x : aT => E)).
   Notation "'\ccnatmul{' x } { n }" := (GRing.natmul x n).
   Notation "'\ccnatmulr{' n }" := (n%:R)%R.
   Notation "'\cczptrunk{' x }" := (Zp_trunc x).

.. raw:: html

   <div>
       \(\newcommand{\cceq}[2]{#1 \,\,=\!\!\!\!=\,\, #2}\)
       \(\newcommand{\ccneq}[2]{#1 \,\,\neq\,\, #2}\)
       \(\newcommand{\ccandb}{\,\,\&\&\,\,}\)
       \(\newcommand{\ccpolyX}{\texttt{X}}\)
       \(\newcommand{\ccpolyXn}[1]{\texttt{X}^{#1}}\)
       \(\newcommand{\ccelem}[2]{[{#1}]'_{#2}}\)
       \(\newcommand{\ccordz}{0}\)
       \(\newcommand{\rtimes}{\times}\)
       \(\newcommand{\ccQ}{\mathbb{Q}}\)
       \(\newcommand{\ccNat}{\mathbb{N}}\)
       \(\newcommand{\ccord}[1]{\mathbb{I}_{#1}}\)
       \(\newcommand{\ccordinal}[1]{\texttt{Ordinal}\,\,{#1}}\)
       \(\newcommand{\ccSucc}[1]{#1 \texttt{+1}}\)
       \(\newcommand{\ccltn}[2]{#1 < #2}\)
       \(\newcommand{\ccSucct}[1]{{#1} \texttt{+2}}\)
       \(\newcommand{\ccpred}[1]{#1 \texttt{-1}}\)
       \(\newcommand{\ccFrac}[2]{\frac{#1}{#2}}\)
       \(\newcommand{\ccPow}[2]{{#1}^{#2}}\)
       \(\newcommand{\ccbin}[2]{{{#1} \choose {#2}}}\)
       \(\newcommand{\ccPowr}[2]{{#1}^{#2}}\)
       \(\newcommand{\ccNot}[1]{{\lnot #1}}\)
       \(\newcommand{\ccEvar}[1]{\textit{\texttt{#1}}}\)
       \(\newcommand{\ccForall}[2]{
         \begin{align}\forall & \: #1.\\& #2 \end{align}}\)
       \(\newcommand{\ccExists}[2]{\exists \: #1. \; #2}\)
       \(\newcommand{\ccbExists}[2]{[\exists \: #1. \; #2]}\)
       \(\newcommand{\ccNsum}[3]{\sum_{#1 < #2} #3}\)
       \(\newcommand{\ccRsum}[3]{\sum_{#1 < #2} #3}\)
       \(\newcommand{\ccNsumd}[4]{\sum_{#1 \le #2 < #3} #4}\)
       \(\newcommand{\ccRsumd}[4]{\sum_{#1 \le #2 < #3} #4}\)
       \(\newcommand{\ccNsumo}[2]{\sum_{#1} #2}\)
       \(\newcommand{\ccRsumo}[2]{\sum_{#1} #2}\)
       \(\newcommand{\ccRsumod}[4]{\sum_{#1 | #2 \neq #3} #4}\)
       \(\newcommand{\ccNprod}[3]{\prod_{#1 < #2} #3}\)
       \(\newcommand{\ccRprod}[3]{\prod_{#1 < #2} #3}\)
       \(\newcommand{\ccdigitn}[3]{{\texttt D}_{#1}[#2, #3]}\)
       \(\newcommand{\ccmodn}[2]{{#1}\!\!\!\mod{#2}}\)
       \(\newcommand{\ccmodneq}[3]{{#1} \quad = \quad {#2} \qquad (\mathrm{mod}{#3})}\)
       \(\newcommand{\ccdvdn}[2]{{#1}\,\, | \,\, {#2}}\)
       \(\newcommand{\ccdivn}[2]{{#1}\,\, / \,\, {#2}}\)
       \(\newcommand{\ccpoly}[1]{\{ \texttt{poly}\,\, #1\}}\)
       \(\newcommand{\ccprime}[1]{\texttt{prime}(#1)}\)
       \(\newcommand{\ccbump}[2]{\texttt{bump}(#1, #2)}\)
       \(\newcommand{\cclift}[2]{\texttt{lift}(#1, #2)}\)
       \(\newcommand{\ccapp}[2]{#1(#2)}\)
       \(\newcommand{\ccfp}[1]{\mathbb{F}_{#1}}\)
       \(\newcommand{\ccffun}[1]{\{\texttt{ffun}\ {#1}\}}\)
       \(\newcommand{\ccdffun}[3]{[\texttt{ffun}\,\, {#1} :\,\, {#2} \Rightarrow{} {#3}]}\)
       \(\newcommand{\ccnatmul}[2]{{#1}\,\, \texttt{*+}\,\,{#2}}\)
       \(\newcommand{\ccnatmulr}[1]{({#1})\texttt{:R}}\)
       \(\newcommand{\cczptrunk}[1]{\texttt{Zp_trunc}(#1)}\)
       \(\newcommand{\ccltnpdigit}[3]{\texttt{ltn_pdiv}(#1,#2,#3)}\)
       \(\newcommand{\ccprimegtz}[1]{\texttt{prime_gt0}(#1)}\)

   </div>

   <script type="text/javascript">
     function setup() {
        var spans = document.querySelectorAll(".goal-conclusion .highlight, .goal-hyp .highlight");
        spans.forEach(function (e) {
            var text = e.innerText;
            var node = document.createTextNode('\\[' + text + '\\]');
            e.parentNode.replaceChild(node, e);
        });
     }

     MathJax = {
         options: {
             skipHtmlTags: [
                 'script', 'noscript', 'style', 'textarea',
                 'annotation', 'annotation-xml'
             ]
         },
         startup: {
             pageReady: function () {
                 setup();
                 return MathJax.startup.defaultPageReady();
             }
         }
     };
   </script>

   <style type="text/css"> /* Override MathJax margins */
       .hyp-type > *, .goal-conclusion > * {
           margin: 0 !important;
       }
   </style>

   <script type="text/javascript" id="MathJax-script" async
      src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js">
   </script>

.. coq:: all unfold

   Set Implicit Arguments.
   Unset Strict Implicit.
   Unset Printing Implicit Defensive.


   Import GRing.Theory.
   Local Open Scope ring_scope.

   Section ExtraLemma.

   Variable p : nat.
   Hypothesis Pp : prime p.


   Lemma Fp_exprnD (p1 p2 : {poly 'F_p}) : (p1 + p2) ^+ p = p1 ^+ p + p2 ^+ p.
   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.

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

   End ExtraLemma.