From mathcomp Require Import all_ssreflect  all_algebra all_fingroup all_field.

Search Monoid.law.
Locate Monoid.law.
Section Agrawal.
 Variables (n':nat).
Definition n : nat := n'.+2.

Open Scope ring_scope.

(*Lemma aux : forall (n : nat), prime n -> \sum_(1 <= i < n) (@polyC [ringType of {poly 'F_n}] 0) = (@polyC [ringType of {poly 'F_n}] 0).
Proof.
  induction n0; first by move=> pn.
  move=> pn.
    rewrite big_nat_recr//=.
    rewrite GRing.addr0.
    admit.
    assert (n0.+1 >= 2)%N; first by exact: prime_gt1.
    by rewrite ltnSS.
Admitted.
*)
Check [idomainType of 'F_n].
Lemma EulerFermatPoly : forall (a : 'F_n), prime n -> (polyC a)^+n = polyC a.
Admitted.
Lemma agrawal_biswas: forall (a : 'F_n), prime n <-> (('X + a%:P)^+n = 'X^n + a%:P).
Proof.
  move=> a; split.
  move=> pn.
  Search binomial.
  Search  'C(_,_) .
  rewrite GRing.exprDn.
  Search "rec" "big".
  move: (pn).
  move/prime_dvd_bin => n_dvd_coef.
  Check ( \sum_(i < n.+1) 'X^(n - i) * a%:P ^+ i *+ 'C(n, i)).
  Search  "big_mkord".
  Locate "\sum_".
  Search bump.
  rewrite big_ord_recl//=.

  rewrite bin0.
  rewrite big_ord_recr //=.
  rewrite subn0.
  rewrite GRing.expr0 GRing.mulr1 GRing.mulr1n //=.
  rewrite/bump//=.
  rewrite(_ : (1 + n'.+1 = n)%N).
  rewrite subnn//= !binn GRing.expr0//= GRing.mul1r GRing.mulr1n//=.
  rewrite EulerFermatPoly //.
  rewrite(_ : \sum_(i < n'.+1) 'X^(n - (1 + i)) * a%:P^+ (1 + i) *+ 'C(n, 1 + i) = 0%:P) //=; first by rewrite GRing.add0r.
  rewrite(_ : \sum_(i < n'.+1) 'X^(n - (1 + i)) * a%:P^+ (1 + i) *+ 'C(n, 1 + i)  = \sum_(i < n'.+1) 0%:P); first by apply/big1.
  Search "big".
  rewrite(_ :  \sum_(i < n'.+1) 'X^(n - (1 + i)) * a%:P ^+ (1 + i) *+ 'C(n, 1 + i) =  \sum_(0 <= i < n'.+1) 'X^(n - (1 + i)) * a%:P ^+ (1 + i) *+ 'C(n, 1 + i)).
  rewrite(_ :  \sum_(i < n'.+1) 0%:P =  \sum_(0 <= i < n'.+1) 0%:P).
  Search "big" "eq".
  apply/eq_big_nat.
  move=> i range.
  rewrite(_ : 1 + i = i.+1)%N.
  have range_Si : (1 <= i.+1 < n)%N; first by rewrite /n; exact: range.
  have S_i_dvd_n : (n %| 'C(n, i.+1))%N. by apply/n_dvd_coef.
  move: (S_i_dvd_n).
  Check dvdnP.
  move/dvdnP => Hip_A.
  destruct Hip_A.
  rewrite H.