Library poly

 This file provides a library for univariate polynomials over ring          
 structures; it also provides an extended theory for polynomials whose      
 coefficients range over commutative rings and integral domains.            

           {poly R} == the type of polynomials with coefficients of type R, 
                       represented as lists with a non zero last element    
                       (big endian representation); the coeficient type R   
                       must have a canonical ringType structure cR. In fact 
                       {poly R} denotes the concrete type polynomial cR; R  
                       is just a phantom argument that lets type inference  
                       reconstruct the (hidden) ringType structure cR.      
          p : seq R == the big-endian sequence of coefficients of p, via    
                       the coercion polyseq: polynomial >-> seq.            
             Poly s == the polynomial with coefficient sequence s (ignoring 
                       trailing zeroes).                                    
 \poly_(i < n) E(i) == the polynomial of degree at most n - 1 whose         
                       coefficients are given by the general term E(i)      
   0, 1, -p, p + q, == the usual ring operations: {poly R} has a canonical  
 p * q, p ^+ n, ...    ringType structure, which is commutative / integral  
                       when R is commutative / integral, respectively.      
               c%:P == the constant polynomial c                            
                 'X == the (unique) variable                                
               'X^n == a power of 'X; 'X^0 is 1, 'X^1 is convertible to 'X  
               p`_i == the coefficient of 'X^i in p; this is in fact just   
                       the ring_scope notation generic seq-indexing using   
                       nth 0%R, combined with the polyseq coercion.         
             size p == 1 + the degree of p, or 0 if p = 0 (this is the      
                       generic seq function combined with polyseq).         
        lead_coef p == the coefficient of the highest monomial in p, or 0   
                       if p = 0 (hence lead_coef p = 0 iff p = 0)           
            monic p == p is monic, i.e., lead_coef p = 1 (0 is not monic)   
             p.[x]  == the evaluation of a polynomial p at a point x using  
                       the Horner scheme                                    
*** The multi-rule horner_lin (resp. horner_lin_com)
                       unwinds horner evaluation of a polynomial expression 
                       (resp. in a non commutative ring, under appropriate  
                       assumptions).                                        
             p^`()  == formal derivative of p                               
             p^`(n) == formal n-derivative of p                             
            p^`N(n) == formal n-derivative of p divided by n!               
            p \Po q == polynomial composition                               
                       \sum(i< size p) p`_i *: q^+i                         
       com_poly p x == x and p.[x] commute; this is a sufficient condition  
                       for evaluating (q * p).[x] as q.[x] * p.[x] when R   
                       is not commutative.                                  
       com_coef p x == x commutes with all the coefficients of p (clearly,  
                       this implies com_poly p x).                          
           root p x == x is a root of p, i.e., p.[x] = 0                    
    n.-unity_root x == x is an nth root of unity, i.e., a root of 'X^n - 1  
 n.-primitive_root x == x is a primitive nth root of unity, i.e., n is the  
                       least positive integer m > 0 such that x ^+ m = 1.   
*** The submodule poly.UnityRootTheory can be used to
                       import selectively the part of the theory of roots   
                       of unity that doesn't mention polynomials explicitly 
       map_poly f p == the image of the polynomial by the function f (which 
                       should be a ring morphism).                          
     comm_ringM f u == u commutes with the image of f (i.e., with all f x)  
   horner_morph f u == the function mapping p to the value of map_poly f p  
                       at u; this is a morphism from {poly R} to the image  
                       ring of f when f is a morphism and comm_ringM f u.   
  We define pseudo division on polynomials over an integral domain :        
             m %/ d == the pseudo-quotient                                  
             m %% d == the pseudo remainder                                 
          scalp m d == the scaling coefficient of the pseudo-division       
             p %| q <=> q is a pseudo-divisor of p                          
             p %= q <=> p and q are equal up to a non-zero scalar factor    
                    := (p %| q) && (q %| p)                                 
*** If R is a field, this means p and q are associate.
           gcdp p q == pseudo-gcd of p and q. This is defined for p and q   
                       with coefficients in an arbitrary ring; however gcdp 
                       is only known to be idempotent and  associative when 
                       R has an integral domain (idomainType) structure.    
     diff_roots x y == x and y are distinct roots; if R is a field, this    
                       just means x != y, but this concept is generalized   
                       to the case where R is only a ring with units (i.e., 
                       a unitRingType); in which case it means that x and y 
                       commute, and that the difference x - y is a unit     
                       (i.e., has a multiplicative inverse) in R.           
                       to just x != y).                                     
       uniq_roots s == s is a sequence or pairwise distinct roots, in the   
                       sense of diff_roots p above.                         
*** We only show that these operations and properties are transferred by
       morphisms whose domain is a field (thus ensuring injectivity).       
 We prove the factor_theorem, and the max_poly_roots inequality relating    
 the number of distinct roots of a polynomial and its size.                 


Import GRing.Theory.
Open Local Scope ring_scope.

Reserved Notation "{ 'poly' T }" (at level 0, format "{ 'poly' T }").
Reserved Notation "c %:P" (at level 2, format "c %:P").
Reserved Notation "'X" (at level 0).
Reserved Notation "''X^' n" (at level 3, n at level 2, format "''X^' n").
Reserved Notation "\poly_ ( i < n ) E"
  (at level 36, E at level 36, i, n at level 50,
   format "\poly_ ( i < n ) E").
Reserved Notation "p %= q" (at level 70, no associativity).
Reserved Notation "a ^`N ( n )" (at level 8, format "a ^`N ( n )").
Reserved Notation "n .-unity_root" (at level 2, format "n .-unity_root").
Reserved Notation "n .-primitive_root"
  (at level 2, format "n .-primitive_root").

Local Notation simp := Monoid.simpm.

 left and right regularity -> ssalg 
Section Ring.

Variable R : ringType.

Definition lreg a := forall b: R, a * b = 0 -> b = 0.
Definition rreg a := forall b: R, b * a = 0 -> b = 0.

Lemma lreg0 : ~ lreg 0.

Lemma rreg0 : ~ rreg 0.

Lemma lreg1 : lreg 1.

Lemma rreg1 : rreg 1.

Lemma lregM : forall a b, lreg a -> lreg b -> lreg (a * b).

Lemma rregM : forall a b, rreg a -> rreg b -> rreg (a * b).

Lemma lregX : forall a n, lreg a -> lreg (a ^+ n).

Lemma rregX : forall a n, rreg a -> rreg (a ^+ n).

End Ring.

Section IRing.

Variables (R : idomainType) (a : R).

Lemma lregP : reflect (lreg a) (a != 0).

Lemma rregP : reflect (rreg a) (a != 0).

End IRing.

Section Polynomial.

Variable R : ringType.

 Defines a polynomial as a sequence with <> 0 last element 
Record polynomial := Polynomial {polyseq :> seq R; _ : last 1 polyseq != 0}.

Canonical Structure polynomial_subType :=
  Eval hnf in [subType for polyseq by polynomial_rect].
Definition polynomial_eqMixin := Eval hnf in [eqMixin of polynomial by <:].
Canonical Structure polynomial_eqType :=
  Eval hnf in EqType polynomial polynomial_eqMixin.
Definition polynomial_choiceMixin := [choiceMixin of polynomial by <:].
Canonical Structure polynomial_choiceType :=
  Eval hnf in ChoiceType polynomial polynomial_choiceMixin.

Lemma poly_inj : injective polyseq.

Definition poly_of of phant R := polynomial.
Identity Coercion type_poly_of : poly_of >-> polynomial.

End Polynomial.

 We need to break off the section here to let the argument scope 
 directives take effect.                                         
Notation "{ 'poly' T }" := (poly_of (Phant T)).

Section PolynomialTheory.

Variable R : ringType.

Implicit Types p q : {poly R}.

Canonical Structure poly_subType := Eval hnf in [subType of {poly R}].
Canonical Structure poly_eqType := Eval hnf in [eqType of {poly R}].
Canonical Structure poly_choiceType := Eval hnf in [choiceType of {poly R}].

Definition lead_coef p := p`_(size p).-1.
Lemma lead_coefE : forall p, lead_coef p = p`_(size p).-1.

Definition polyC c : {poly R} :=
  insubd (@Polynomial R [::] (nonzero1r _)) [:: c].

Local Notation "c %:P" := (polyC c).

 Remember the boolean (c != 0) is coerced to 1 if true and 0 if false 
Lemma polyseqC : forall c, c%:P = nseq (c != 0) c :> seq R.

Lemma size_polyC : forall c, size c%:P = (c != 0).

Lemma coefC : forall c i, c%:P`_i = if i == 0%N then c else 0.

Lemma polyC_inj : injective polyC.

Lemma lead_coefC : forall c, lead_coef c%:P = c.

 Extensional interpretation (poly <=> nat -> R) 
Lemma polyP : forall p1 p2, nth 0 p1 =1 nth 0 p2 <-> p1 = p2.

Lemma size1_polyC : forall p, size p <= 1 -> p = (p`_0)%:P.

 Builds a polynomial by extension. 
Definition poly_cons c p : {poly R} :=
  if p is Polynomial ((_ :: _) as s) ns then
     @Polynomial R (c :: s) ns
  else c%:P.

Lemma polyseq_cons : forall c p,
  poly_cons c p = (if size p != 0%N then c :: p else c%:P) :> seq R.

Lemma size_poly_cons : forall c p,
  size (poly_cons c p) =
    (if (size p == 0%N) && (c == 0) then 0%N else (size p).+1).

Lemma coef_cons : forall c p i,
  (poly_cons c p)`_i = if i == 0%N then c else p`_i.-1.

 Builds a polynomial from a bare list of coefficients 
Definition Poly := foldr poly_cons 0%:P.

Lemma PolyK : forall c s, last c s != 0 -> Poly s = s :> seq R.

Lemma polyseqK : forall p, Poly p = p.

Lemma size_Poly : forall s, size (Poly s) <= size s.

Lemma coef_Poly : forall s i, (Poly s)`_i = s`_i.

 Builds a polynomial from an infinite seq of coef and a bound 
Local Notation "\poly_ ( i < n ) E" := (Poly (mkseq (fun i : nat => E) n)).

Lemma polyseq_poly : forall n E,
  E n.-1 != 0 -> \poly_(i < n) E i = mkseq [eta E] n :> seq R.

Lemma size_poly : forall n E, size (\poly_(i < n) E i) <= n.

Lemma size_poly_eq : forall n E, E n.-1 != 0 -> size (\poly_(i < n) E i) = n.

Lemma coef_poly : forall n E k,
  (\poly_(i < n) E i)`_k = (if k < n then E k else 0).

Lemma lead_coef_poly : forall n E,
  n > 0 -> E n.-1 != 0 -> lead_coef (\poly_(i < n) E i) = E n.-1.

Lemma coefK : forall p, \poly_(i < size p) p`_i = p.

 Zmodule structure for polynomial 
Definition add_poly p1 p2 :=
  \poly_(i < maxn (size p1) (size p2)) (p1`_i + p2`_i).

Definition opp_poly p := \poly_(i < size p) - p`_i.

Lemma coef_add_poly : forall p1 p2 i, (add_poly p1 p2)`_i = p1`_i + p2`_i.

Lemma coef_opp_poly : forall p i, (opp_poly p)`_i = - p`_i.

Lemma add_polyA : associative add_poly.

Lemma add_polyC : commutative add_poly.

Lemma add_poly0 : left_id 0%:P add_poly.

Lemma add_poly_opp : left_inverse 0%:P opp_poly add_poly.

Definition poly_zmodMixin :=
  ZmodMixin add_polyA add_polyC add_poly0 add_poly_opp.
Canonical Structure poly_zmodType :=
  Eval hnf in ZmodType {poly R} poly_zmodMixin.
Canonical Structure polynomial_zmodType :=
  Eval hnf in [zmodType of polynomial R for poly_zmodType].

 Properties of the zero polynomial 

Lemma polyC0 : 0%:P = 0 :> {poly R}.

Lemma seq_poly0 : (0 : {poly R}) = [::] :> seq R.

Lemma size_poly0 : size (0 : {poly R}) = 0%N.

Lemma coef0 : forall i, (0 : {poly R})`_i = 0.

Lemma lead_coef0 : lead_coef 0 = 0.

Lemma size_poly_eq0 : forall p, (size p == 0%N) = (p == 0).

Lemma poly0Vpos : forall p, {p = 0} + {size p > 0}.

Lemma polySpred : forall p, p != 0 -> size p = (size p).-1.+1.

Lemma lead_coef_eq0 : forall p, (lead_coef p == 0) = (p == 0).

Lemma polyC_eq0 : forall c, (c%:P == 0) = (c == 0).

 Size, leading coef, morphism properties of coef 
Lemma leq_size_coef : forall p i,
  (forall j, i <= j -> p`_j = 0) -> size p <= i.

Lemma leq_coef_size : forall p i, p`_i != 0 -> i < size p.

Lemma coef_add : forall p1 p2 i, (p1 + p2)`_i = p1`_i + p2`_i.

Lemma coef_opp : forall p i, (- p)`_i = - p`_i.

Lemma coef_sub : forall p1 p2 i, (p1 - p2)`_i = p1`_i - p2`_i.

Lemma coef_natmul : forall p n i, (p *+ n)`_i = p`_i *+ n.

Lemma coef_negmul : forall p n i, (p *- n)`_i = p`_i *- n.

Lemma coef_sum : forall I r (P : pred I) (F : I -> {poly R}) k,
  (\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k.

Lemma polyC_add : {morph polyC : c1 c2 / c1 + c2}.

Lemma polyC_opp : {morph polyC : c / - c}.

Lemma polyC_sub : {morph polyC : c1 c2 / c1 - c2}.

Lemma polyC_natmul : forall n, {morph polyC : c / c *+ n}.

Lemma size_opp : forall p, size (- p) = size p.

Lemma lead_coef_opp : forall p, lead_coef (- p) = - lead_coef p.

Lemma size_add : forall p q, size (p + q) <= maxn (size p) (size q).

Lemma size_addl : forall p q, size p > size q -> size (p + q) = size p.

Lemma size_sum : forall I r (P : pred I) (F : I -> {poly R}),
  size (\sum_(i <- r | P i) F i) <= \max_(i <- r | P i) size (F i).

Lemma lead_coef_addl : forall p q,
  size p > size q -> lead_coef (p + q) = lead_coef p.

 And now the Ring structure. 

Definition mul_poly p1 p2 :=
  \poly_(i < (size p1 + size p2).-1) (\sum_(j < i.+1) p1`_j * p2`_(i - j)).

Lemma coef_mul_poly : forall p1 p2 i,
  (mul_poly p1 p2)`_i = \sum_(j < i.+1) p1`_j * p2`_(i - j)%N.

Lemma coef_mul_poly_rev : forall p1 p2 i,
  (mul_poly p1 p2)`_i = \sum_(j < i.+1) p1`_(i - j)%N * p2`_j.

Lemma mul_polyA : associative mul_poly.

Lemma mul_1poly : left_id 1%:P mul_poly.

Lemma mul_poly1 : right_id 1%:P mul_poly.

Lemma mul_poly_addl : left_distributive mul_poly +%R.

Lemma mul_poly_addr : right_distributive mul_poly +%R.

Lemma nonzero_poly1 : 1%:P != 0.

Definition poly_ringMixin :=
  RingMixin mul_polyA mul_1poly mul_poly1 mul_poly_addl mul_poly_addr
            nonzero_poly1.
Canonical Structure poly_ringType :=
  Eval hnf in RingType {poly R} poly_ringMixin.
Canonical Structure polynomial_ringType :=
  Eval hnf in [ringType of polynomial R for poly_ringType].

Lemma polyC1 : 1%:P = 1.

Lemma polyseq1 : (1 : {poly R}) = [:: 1] :> seq R.

Lemma size_poly1 : size (1 : {poly R}) = 1%N.

Lemma coef1 : forall i, (1 : {poly R})`_i = (i == 0%N)%:R.

Lemma lead_coef1 : lead_coef 1 = 1.

Lemma coef_mul : forall p1 p2 i,
  (p1 * p2)`_i = \sum_(j < i.+1) p1`_j * p2`_(i - j)%N.

Lemma coef_mul_rev : forall p1 p2 i,
  (p1 * p2)`_i = \sum_(j < i.+1) p1`_(i - j)%N * p2`_j.

Lemma size_mul : forall p1 p2, size (p1 * p2) <= (size p1 + size p2).-1.

Lemma head_coef_mul : forall p q,
  (p * q)`_(size p + size q).-2 = lead_coef p * lead_coef q.

Lemma size_proper_mul : forall p q,
  lead_coef p * lead_coef q != 0 -> size (p * q) = (size p + size q).-1.

Lemma lead_coef_proper_mul : forall p q,
  let c := lead_coef p * lead_coef q in c != 0 -> lead_coef (p * q) = c.

Lemma size_exp : forall p n, size (p ^+ n) <= ((size p).-1 * n).+1.

Lemma size_sign_mul : forall p n, size ((-1) ^+ n * p) = size p.

Lemma coef_Cmul : forall c p i, (c%:P * p)`_i = c * p`_i.

Lemma coef_mulC : forall c p i, (p * c%:P)`_i = p`_i * c.

Lemma polyC_mul : {morph polyC : c1 c2 / c1 * c2}.

Lemma polyC_exp : forall n, {morph polyC : c / c ^+ n}.

Definition scale_poly a p := \poly_(i < size p) (a * p`_i).

Lemma scale_polyE : forall a p, scale_poly a p = a%:P * p.

Lemma scale_polyA : forall a b p,
  scale_poly a (scale_poly b p) = scale_poly (a * b) p.

Lemma scale_1poly : left_id 1 scale_poly.

Lemma scale_poly_addr : forall a, {morph scale_poly a : p q / p + q}.

Lemma scale_poly_addl : forall p, {morph scale_poly^~ p : a b / a + b}.

Lemma scale_poly_mull : forall a p q, scale_poly a (p * q) = scale_poly a p * q.

Canonical Structure poly_lmodMixin :=
  LmodMixin scale_polyA scale_1poly scale_poly_addr scale_poly_addl.
Canonical Structure poly_lmodType :=
  Eval hnf in LmodType R {poly R} poly_lmodMixin.
Canonical Structure polynomial_lmodType :=
  Eval hnf in [lmodType R of polynomial R for poly_lmodType].
Canonical Structure poly_lalgType :=
  Eval hnf in LalgType R {poly R} scale_poly_mull.
Canonical Structure polynomial_lalgType :=
  Eval hnf in [lalgType R of polynomial R for poly_lalgType].

Lemma mul_polyC : forall a p, a%:P * p = a *: p.

Lemma scale_poly1 : forall a, a *: 1 = a%:P.

Lemma coef_scaler : forall a p i, (a *: p)`_i = a * (p`_i).

 Indeterminate, at last! 

Definition polyX := Poly [:: 0; 1].

Local Notation "'X" := polyX.

Lemma polyseqX : 'X = [:: 0; 1] :> seq R.

Lemma size_polyX : size 'X = 2.

Lemma coefX : forall i, 'X`_i = (i == 1%N)%:R.

Lemma lead_coefX : lead_coef 'X = 1.

Lemma commr_polyX : forall p, GRing.comm p 'X.

Lemma coef_mulX : forall p i, (p * 'X)`_i = (if (i == 0)%N then 0 else p`_i.-1).

Lemma coef_Xmul : forall p i, ('X * p)`_i = (if (i == 0)%N then 0 else p`_i.-1).

Lemma poly_cons_def : forall p a, poly_cons a p = p * 'X + a%:P.

Lemma size_amulX : forall p c,
   size (p * 'X + c%:P) =
     (if (size p == 0%N) && (c == 0) then 0%N else (size p).+1).

Lemma poly_ind : forall K : {poly R} -> Type,
  K 0 -> (forall p c, K p -> K (p * 'X + c%:P)) -> (forall p, K p).

Lemma seq_mul_polyX : forall p, p != 0 -> p * 'X = 0 :: p :> seq R.

Lemma lead_coef_mulX : forall p, lead_coef (p * 'X) = lead_coef p.

Local Notation "''X^' n" := ('X ^+ n).

Lemma coef_Xn : forall n i, 'X^n`_i = (i == n)%:R.

Lemma seq_polyXn : forall n, 'X^n = ncons n 0 [:: 1] :> seq R.

Lemma size_polyXn : forall n, size 'X^n = n.+1.

Lemma commr_polyXn : forall p n, GRing.comm p 'X^n.

Lemma lead_coefXn : forall n, lead_coef 'X^n = 1.

Lemma coef_Xn_mul : forall n p i,
  ('X^n * p)`_i = if i < n then 0 else p`_(i - n).

Lemma coef_mulXn : forall n p i,
  (p * 'X^n)`_i = if i < n then 0 else p`_(i - n).

 Expansion of a polynomial as an indexed sum 
Lemma poly_def : forall n E, \poly_(i < n) E i = \sum_(i < n) E i *: 'X^i.

 Monic predicate 

Definition monic p := lead_coef p == 1.

Lemma monic1 : monic 1.

Lemma monicX : monic 'X.

Lemma monicXn : forall n, monic 'X^n.

Lemma monic_neq0 : forall p, monic p -> p != 0.

Lemma lead_coef_monic_mul : forall p q,
  monic p -> lead_coef (p * q) = lead_coef q.

Lemma lead_coef_mul_monic : forall p q,
  monic q -> lead_coef (p * q) = lead_coef p.

Lemma size_monic_mul : forall p q,
  monic p -> q != 0 -> size (p * q) = (size p + size q).-1.

Lemma size_mul_monic : forall p q,
  p != 0 -> monic q -> size (p * q) = (size p + size q).-1.

Lemma monic_mull : forall p q, monic p -> monic (p * q) = monic q.

Lemma monic_mulr : forall p q, monic q -> monic (p * q) = monic p.

Lemma monic_exp : forall p n, monic p -> monic (p ^+ n).

 Pseudo division, defined on an arbitrary ring 
Definition edivp_rec (q : {poly R}) :=
  let sq := size q in
  let cq := lead_coef q in
  fix loop (n : nat) (k : nat) (qq r : {poly R}) {struct n} :=
    if size r < sq then (k, qq, r) else
    let m := (lead_coef r)%:P * 'X^(size r - sq) in
    let qq1 := qq * cq%:P + m in
    let r1 := r * cq%:P - m * q in
    if n is n1.+1 then loop n1 k.+1 qq1 r1 else (k.+1, qq1, r1).

Definition edivp (p q : {poly R}) : nat * {poly R} * {poly R} :=
  if q == 0 then (0%N, 0, p) else edivp_rec q (size p) 0 0 p.

CoInductive edivp_spec (m d : {poly R}) : nat * {poly R} * {poly R} -> Type :=
  EdivnSpec k (q r: {poly R}) of
   (GRing.comm d (lead_coef d)%:P -> m * (lead_coef d ^+ k)%:P = q * d + r) &
   (d != 0 -> size r < size d) : edivp_spec m d (k, q, r).

Lemma edivpP : forall m d, edivp_spec m d (edivp m d).

 Some fact about regular elements 

Lemma lreg_lead: forall p, lreg (lead_coef p) -> lreg p.

Lemma rreg_lead: forall p, rreg (lead_coef p) -> rreg p.

Lemma lreg_lead0: forall p, lreg (lead_coef p) -> p != 0.

Lemma rreg_lead0: forall p, rreg (lead_coef p) -> p != 0.

Lemma lreg_scale0: forall c p, lreg c -> (c *: p == 0) = (p == 0).

Lemma rreg_scale0: forall c p, rreg c -> (p * c%:P == 0) = (p == 0).

Lemma lreg_size: forall c p, lreg c -> size (c *: p) = size p.

Lemma rreg_size: forall c p, rreg c -> size (p * (c%:P)) = size p.

Lemma rreg_div0: forall q r d: {poly R}, rreg (lead_coef d) ->
  size r < size d -> (q * d + r == 0) = (q == 0) && (r == 0).

Lemma edivp_eq : forall d q r: {poly R},
  GRing.comm d (lead_coef d)%:P -> rreg (lead_coef d) -> size r < size d ->
  let k := (edivp (q * d + r) d).1.1 in
  let c := (lead_coef d ^+ k)%:P in
  edivp (q * d + r) d = (k, q * c, r * c).

Definition divp p q := ((edivp p q).1).2.
Definition modp p q := (edivp p q).2.
Definition scalp p q := ((edivp p q).1).1.
Definition dvdp p q := modp q p == 0.

Local Notation "m %/ d" := (divp m d) : ring_scope.
Local Notation "m %% d" := (modp m d) : ring_scope.
Local Notation "p %| q" := (dvdp p q) : ring_scope.

 Equality up to a constant factor; this is only used when R is integral 
Definition eqp p q := (p %| q) && (q %| p).

Lemma divp_size : forall p q, size p < size q -> p %/ q = 0.

Lemma modp_size : forall p q, size p < size q -> p %% q = p.

Lemma divp_spec :
  forall p q, GRing.comm q (lead_coef q)%:P ->
  p * (lead_coef q ^+ scalp p q)%:P = p %/ q * q + p %% q.

Lemma divp_mon_spec : forall p q, monic q-> p = p %/ q * q + p %% q.

Lemma modp_spec : forall p q, q != 0 -> size (p %% q) < size q.

Lemma div0p : forall p, 0 %/ p = 0.

Lemma modp0 : forall p, p %% 0 = p.

Lemma mod0p : forall p, 0 %% p = 0.

Lemma dvdp0 : forall p, p %| 0.

Lemma dvdpP : forall p q, GRing.comm q (lead_coef q)%:P -> rreg (lead_coef q) ->
  reflect (exists nq: nat * {poly R}, p * ((lead_coef q)^+nq.1)%:P= nq.2 * q)
          (q %| p).

Lemma monic_comreg: forall p,
  monic p -> GRing.comm p (lead_coef p)%:P /\ rreg (lead_coef p).

Lemma dvdMpP : forall p q, monic q -> reflect (exists qq, p = qq * q) (q %| p).

Lemma divp_mon_eq : forall d q r: {poly R}, monic d -> size r < size d ->
  (q * d + r) %/ d = q.

Lemma modMp_eq : forall d q r: {poly R}, monic d -> size r < size d ->
  (q * d + r) %% d = r.

Lemma size_dvdMp_leqif : forall p q : {poly R},
    monic p -> p %| q -> q != 0 ->
  size p <= size q ?= iff (q == lead_coef q *: p).

Lemma modpC : forall p c, c != 0 -> p %% c%:P = 0.

Lemma modp1 : forall p, p %% 1 = 0.

Lemma divp1 : forall p, p %/ 1 = p.

Lemma dvd1p : forall p, 1 %| p.

Lemma rreg_dvdp_mull : forall p q,
  GRing.comm q (lead_coef q)%:P -> rreg (lead_coef q) -> q %| p * q.

Lemma monic_divp_mull : forall p q, monic q -> p * q %/ q = p.

Lemma monic_modp_add : forall p q m, monic m -> (p + q) %% m = p %% m + q %% m.

Lemma monic_modp_mulmr : forall p q m, monic m -> (p * (q %% m)) %% m = (p * q) %% m.

 Pseudo gcd 
Definition gcdp p q :=
  let: (p1, q1) := if size p < size q then (q, p) else (p, q) in
  if p1 == 0 then q1 else
  let fix loop (n : nat) (pp qq : {poly R}) {struct n} :=
      let rr := pp %% qq in
      if rr == 0 then qq else
      if n is n1.+1 then loop n1 qq rr else rr in
  loop (size p1) p1 q1.

Lemma gcd0p : left_id 0 gcdp.

Lemma gcdp0 : right_id 0 gcdp.

Lemma gcdpE : forall p q,
  gcdp p q = if size p < size q then gcdp (q %% p) p else gcdp (p %% q) q.

End PolynomialTheory.

Notation "{ 'poly' T }" := (poly_of (Phant T)) : type_scope.
Notation "\poly_ ( i < n ) E" := (Poly (mkseq (fun i => E) n)) : ring_scope.
Notation "c %:P" := (polyC c) : ring_scope.
Notation "'X" := (polyX _) : ring_scope.
Notation "''X^' n" := ('X ^+ n) : ring_scope.
Notation "m %/ d" := (divp m d) : ring_scope.
Notation "m %% d" := (modp m d) : ring_scope.
Notation "p %| q" := (dvdp p q) : ring_scope.
Notation "p %= q" := (eqp p q) : ring_scope.

 Horner evaluation of polynomials 

Section EvalPolynomial.

Variable R : ringType.
Implicit Types p q : {poly R}.
Implicit Types x a c : R.

Fixpoint horner s x {struct s} :=
  if s is a :: s' then horner s' x * x + a else 0.

Local Notation "p .[ x ]" := (horner (polyseq p) x) : ring_scope.

Lemma horner0 : forall x, (0 : {poly R}).[x] = 0.

Lemma hornerC : forall c x, (c%:P).[x] = c.

Lemma hornerX : forall x, 'X.[x] = x.

Lemma horner_cons : forall p c x, (poly_cons c p).[x] = p.[x] * x + c.

Lemma horner_amulX : forall p c x, (p * 'X + c%:P).[x] = p.[x] * x + c.

Lemma horner_mulX : forall p x, (p * 'X).[x] = p.[x] * x.

Lemma horner_Poly : forall s x, (Poly s).[x] = horner s x.

Lemma horner_coef : forall p x,
  p.[x] = \sum_(i < size p) p`_i * x ^+ i.

Lemma horner_coef_wide : forall n p x,
  size p <= n -> p.[x] = \sum_(i < n) p`_i * x ^+ i.

Lemma horner_poly : forall n E x,
  (\poly_(i < n) E i).[x] = \sum_(i < n) E i * x ^+ i.

Lemma horner_opp : forall p x, (- p).[x] = - p.[x].

Lemma horner_add : forall p q x, (p + q).[x] = p.[x] + q.[x].

Lemma horner_sum : forall I r (P : pred I) F x,
  (\sum_(i <- r | P i) F i).[x] = \sum_(i <- r | P i) (F i).[x].

Lemma horner_Cmul : forall c p x, (c%:P * p).[x] = c * p.[x].

Lemma horner_scaler : forall c p x, (c *: p).[x] = c * p.[x].

Lemma horner_mulrn : forall n p x, (p *+ n).[x] = p.[x] *+ n.

Definition com_coef p (x : R) := forall i, p`_i * x = x * p`_i.

Definition com_poly p x := x * p.[x] = p.[x] * x.

Lemma com_coef_poly : forall p x, com_coef p x -> com_poly p x.

Lemma com_poly0 : forall x, com_poly 0 x.

Lemma com_poly1 : forall x, com_poly 1 x.

Lemma com_polyX : forall x, com_poly 'X x.

Lemma horner_mul_com : forall p q x,
  com_poly q x -> (p * q).[x] = p.[x] * q.[x].

Lemma horner_exp_com : forall p x n, com_poly p x -> (p ^+ n).[x] = p.[x] ^+ n.

Lemma hornerXn : forall x n, ('X^n).[x] = x ^+ n.

Definition horner_lin_com :=
  (horner_add, horner_opp, hornerX, hornerC, horner_cons,
   simp, horner_Cmul, horner_scaler,
   (fun p x => horner_mul_com p (com_polyX x))).

Lemma factor0 : forall c, ('X - c%:P).[c] = 0.

Lemma seq_factor : forall c, 'X - c%:P = [:: - c; 1] :> seq R.

Lemma monic_factor : forall c, monic ('X - c%:P).

Theorem factor_theorem : forall p c,
  reflect (exists q, p = q * ('X - c%:P)) (p.[c] == 0).

Definition root p : pred R := fun x => p.[x] == 0.

Lemma root_factor_theorem : forall p x, root p x = ('X - x%:P %| p).

Lemma prod_factors_monic : forall rs : seq R,
  monic (\prod_(z <- rs) ('X - z%:P)).

Lemma size_prod_factors : forall rs : seq R,
  size (\prod_(z <- rs) ('X - z%:P)) = (size rs).+1.

Lemma size_Xn_sub_1 : forall n, n > 0 -> size ('X^n - 1 : {poly R}) = n.+1.

Lemma Xn_sub_1_monic : forall n, n > 0 -> monic ('X^n - 1 : {poly R}).

Definition root_of_unity n : pred R := root ('X^n - 1).
Local Notation "n .-unity_root" := (root_of_unity n) : ring_scope.

Lemma unity_rootE : forall n z, n.-unity_root z = (z ^+ n == 1).

Lemma unity_rootP : forall n z, reflect (z ^+ n = 1) (n.-unity_root z).

Definition primitive_root_of_unity n z :=
  (n > 0) && (forallb i : 'I_n, i.+1.-unity_root z == (i.+1 == n)).
Local Notation "n .-primitive_root" := (primitive_root_of_unity n) : ring_scope.

Lemma prim_order_exists : forall n z,
  n > 0 -> z ^+ n = 1 -> {m | m.-primitive_root z & (m %| n)%N}.

Variables (n : nat) (z : R).
Hypothesis prim_z : n.-primitive_root z.

Lemma prim_order_gt0 : n > 0.


Lemma prim_expr_order : z ^+ n = 1.

Lemma prim_expr_mod : forall i, z ^+ (i %% n) = z ^+ i.

Lemma prim_order_dvd : forall i, (n %| i)%N = (z ^+ i == 1).

Lemma eq_prim_root_expr : forall i j, (z ^+ i == z ^+ j) = (i == j %[mod n]).

End EvalPolynomial.

Notation "p .[ x ]" := (horner p x) : ring_scope.
Notation "n .-unity_root" := (root_of_unity n) : ring_scope.
Notation "n .-primitive_root" := (primitive_root_of_unity n) : ring_scope.

Implicit Arguments unity_rootP [R n z].

 Container morphism. 
Section MapPoly.

Variables (aR rR : ringType).

Section Definitions.

Variable f : aR -> rR.

Definition map_poly (p : {poly aR}) := \poly_(i < size p) f p`_i.

 Alternative definition; the one above is more convenient because it lets 
 us use the lemmas on \poly, e.g., size (map_poly p) <= size p is an      
 instance of size_poly.                                                   
Lemma map_polyE : forall p, map_poly p = Poly (map f p).

Definition commr_rmorph u := forall x, GRing.comm u (f x).

Definition horner_morph u of commr_rmorph u := fun p => (map_poly p).[u].

End Definitions.

Section Additive.

Variable f : {additive aR -> rR}.

Local Notation "p ^f" := (map_poly f p) : ring_scope.

Lemma coef_map : forall p i, p^f`_i = f p`_i.

Lemma map_poly_is_additive : additive (map_poly f).

Canonical Structure map_poly_additive := Additive map_poly_is_additive.

Lemma map_polyC : forall a, (a%:P)^f = (f a)%:P.

Lemma lead_coef_map_eq : forall p,
  f (lead_coef p) != 0 -> lead_coef p^f = f (lead_coef p).

End Additive.

Variable f : {rmorphism aR -> rR}.

Local Notation "p ^f" := (map_poly f p) : ring_scope.

Lemma map_poly_is_rmorphism : GRing.rmorphism (map_poly f).
Canonical Structure map_poly_rmorphism := RMorphism map_poly_is_rmorphism.

Lemma map_polyX : ('X)^f = 'X.

Lemma map_polyXn : forall n, ('X^n)^f = 'X^n.

Lemma map_poly_scaler : forall k (p: {poly aR}), (k *: p)^f = f k *: (p^f).

Lemma horner_map : forall p x, p^f.[f x] = f p.[x].

Lemma map_com_poly : forall p x, com_poly p x -> com_poly p^f (f x).

Lemma map_com_coef : forall p x, com_coef p x -> com_coef p^f (f x).

Lemma root_map_poly : forall p x, root p x -> root p^f (f x).

Lemma rmorph_unity_root : forall n z, n.-unity_root z -> n.-unity_root (f z).

Variable u : rR.
Hypothesis cfu : commr_rmorph f u.

Lemma horner_morphC : forall a, horner_morph cfu a%:P = f a.

Lemma horner_morphX : horner_morph cfu 'X = u.

Lemma horner_is_rmorphism : GRing.rmorphism (horner_morph cfu).
Canonical Structure horner_additive := Additive horner_is_rmorphism.
Canonical Structure horner_rmorphism := RMorphism horner_is_rmorphism.

End MapPoly.

 Morphisms from the polynomial ring, and the initiality of polynomials  
 with respect to these.                                                 
Section MorphPoly.

Variable (aR rR : ringType) (pf : {rmorphism {poly aR} -> rR}).

Lemma polyC_is_rmorphism : GRing.rmorphism (@polyC aR).
Canonical Structure polyC_additive := Additive polyC_is_rmorphism.
Canonical Structure polyC_rmorphism := RMorphism polyC_is_rmorphism.

Lemma poly_morphX_comm : commr_rmorph (pf \o @polyC aR) (pf 'X).

Lemma poly_initial : pf =1 horner_morph poly_morphX_comm.

End MorphPoly.

Section PolynomialComRing.

Variable R : comRingType.
Implicit Types p q : {poly R}.

Lemma horner_mul : forall p q x, (p * q).[x] = p.[x] * q.[x].

Lemma horner_exp : forall p x n, (p ^+ n).[x] = p.[x] ^+ n.

Lemma horner_prod : forall I r (P : pred I) (F : I -> {poly R}) x,
  (\prod_(i <- r | P i) F i).[x] = \prod_(i <- r | P i) (F i).[x].

Definition horner_lin :=
  (horner_add, horner_opp, hornerX, hornerC, horner_cons,
   simp, horner_Cmul, horner_scaler, horner_mul).

Lemma poly_mulC : forall p q, p * q = q * p.
Canonical Structure poly_comRingType :=
  Eval hnf in ComRingType {poly R} poly_mulC.
Canonical Structure polynomial_comRingType :=
  Eval hnf in [comRingType of polynomial R for poly_comRingType].

Canonical Structure poly_algType := Eval hnf in CommAlgType R {poly R}.
Canonical Structure polynomial_algType :=
  Eval hnf in [algType R of polynomial R for poly_algType].

 Pseudo-division in a commutative setting 
Lemma divCp_spec : forall p q,
 lead_coef q ^+ scalp p q *: p = p %/ q * q + p %% q.

End PolynomialComRing.

Section PolynomialIdomain.

Variable R : idomainType.
Implicit Types x y : R.
Implicit Types p q r m n d : {poly R}.

Lemma size_mul_id : forall p q,
  p != 0 -> q != 0 -> size (p * q) = (size p + size q).-1.

Lemma size_polyC_mul : forall c p, c != 0 -> size (c%:P * p) = size p.

Lemma size_scaler: forall c p, c != 0 -> size (c *: p) = size p.

Lemma lead_coef_Imul : forall p q,
  lead_coef (p * q) = lead_coef p * lead_coef q.

Lemma scalp_Ineq0 : forall p q, lead_coef q ^+ scalp p q != 0.

 idomain structure on poly 

Lemma poly_idomainMixin : forall p q, p * q = 0 -> (p == 0) || (q == 0).

Lemma scaler_eq0: forall a p, a *: p = 0-> (a == 0) || (p == 0).

Definition poly_unit : pred {poly R} :=
  fun p => (size p == 1%N) && GRing.unit p`_0.

Definition poly_inv p := if poly_unit p then (p`_0)^-1%:P else p.

Lemma poly_mulVp : {in poly_unit, left_inverse 1 poly_inv *%R}.

Lemma poly_intro_unit : forall p q, q * p = 1 -> poly_unit p.

Lemma poly_inv_out : {in predC poly_unit, poly_inv =1 id}.

Definition poly_unitRingMixin :=
  ComUnitRingMixin poly_mulVp poly_intro_unit poly_inv_out.

Canonical Structure poly_unitRingType :=
  Eval hnf in UnitRingType {poly R} poly_unitRingMixin.
Canonical Structure polynomial_unitRingType :=
  Eval hnf in [unitRingType of polynomial R for poly_unitRingType].

Canonical Structure poly_unitAlgType :=
  Eval hnf in [unitAlgType R of {poly R}].
Canonical Structure polynomial_unitAlgType :=
  Eval hnf in [unitAlgType R of polynomial R].

Canonical Structure poly_comUnitRingType :=
  Eval hnf in [comUnitRingType of {poly R}].
Canonical Structure polynomial_comUnitRingType :=
  Eval hnf in [comUnitRingType of polynomial R].

Canonical Structure poly_idomainType :=
  Eval hnf in IdomainType {poly R} poly_idomainMixin.
Canonical Structure polynomial_idomainType :=
  Eval hnf in [idomainType of polynomial R for poly_idomainType].

Lemma size_exp_id : forall p (n : nat),
  (size (p ^+ n)).-1 = ((size p).-1 * n)%N.

Lemma lead_coef_exp_id : forall p (n : nat),
  lead_coef (p ^+ n) = lead_coef p ^+ n.

Lemma modIp_mull : forall p q, p * q %% q = 0.

Lemma modpp : forall p, p %% p = 0.

Lemma dvdpp : forall p, p %| p.

Lemma divp_mull : forall p q, q != 0 ->
  p * q %/ q = lead_coef q ^+ scalp (p * q) q *: p.

Lemma dvdpPc : forall p q,
  reflect (exists c, exists qq, c != 0 /\ c *: p = qq * q) (q %| p).

Lemma size_dvdp : forall p q, q != 0 -> p %| q -> size p <= size q.

Lemma dvdp_mull : forall d m n, d %| n -> d %| m * n.

Lemma dvdp_mulr : forall d m n, d %| m -> d %| m * n.

Lemma dvdp_mul : forall d1 d2 m1 m2 : {poly R},
  d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.

Lemma dvdp_trans : transitive (@dvdp R).

Lemma dvdp_addr : forall m d n, d %| m -> (d %| m + n) = (d %| n).

Lemma dvdp_addl : forall n d m, d %| n -> (d %| m + n) = (d %| m).

Lemma dvdp_add : forall d m n, d %| m -> d %| n -> d %| m + n.

Lemma dvdp_add_eq : forall d m n, d %| m + n -> (d %| m) = (d %| n).

Lemma dvdp_subr : forall d m n, d %| m -> (d %| m - n) = (d %| n).

Lemma dvdp_subl : forall d m n, d %| n -> (d %| m - n) = (d %| m).

Lemma dvdp_sub : forall d m n, d %| m -> d %| n -> d %| m - n.

Lemma dvdp_mod : forall d m n, d %| m -> (d %| n) = (d %| n %% m).

Lemma gcdpp : idempotent (@gcdp R).

Lemma dvdp_gcd2 : forall m n, (gcdp m n %| m) && (gcdp m n %| n).

Lemma dvdp_gcdl : forall m n, gcdp m n %| m.

Lemma dvdp_gcdr : forall m n, gcdp m n %| n.

Lemma dvdp_gcd : forall p m n, p %| gcdp m n = (p %| m) && (p %| n).

 Equality modulo constant factors 

Lemma eqpP : forall m n,
  reflect (exists c1, exists c2, [/\ c1 != 0, c2 != 0 & c1 *: m = c2 *: n])
          (m %= n).

Lemma eqpxx : reflexive (@eqp R).

Lemma eqp_sym : symmetric (@eqp R).

Lemma eqp_trans : transitive (@eqp R).

Lemma eqp0E : forall p, (p %= 0) = (p == 0).

Lemma size_eqp : forall p q, p %= q -> size p = size q.

 Now we can state that gcd is commutative modulo a factor 
Lemma gcdpC : forall p q, gcdp p q %= gcdp q p.

Lemma root_prod_factors : forall rs x,
  root (\prod_(z <- rs) ('X - z%:P)) x = (x \in rs).

End PolynomialIdomain.

Section MapFieldPoly.

Variables (F : fieldType) (R : ringType) (f : {rmorphism F -> R}).

Local Notation "p ^f" := (map_poly f p) : ring_scope.

Lemma size_map_poly : forall p, size p^f = size p.

Lemma lead_coef_map : forall p, lead_coef p^f = f (lead_coef p).

Lemma map_poly_eq0 : forall p, (p^f == 0) = (p == 0).

Lemma map_poly_inj : injective (map_poly f).

Lemma map_field_poly_monic : forall p, monic p^f = monic p.

Lemma map_poly_com : forall p x, com_poly p^f (f x).

Lemma root_field_map_poly : forall p x, root p^f (f x) = root p x.

Lemma edivp_map : forall p q,
  edivp p^f q^f = (scalp p q, (p %/ q)^f, (p %% q)^f).

Lemma scalp_map : forall p q, scalp p^f q^f = scalp p q.

Lemma map_divp : forall p q, (p %/ q)^f = p^f %/ q^f.

Lemma map_modp : forall p q, (p %% q)^f = p^f %% q^f.

Lemma dvdp_map : forall p q, (p^f %| q^f) = (p %| q).

Lemma eqp_map : forall p q, (p^f %= q^f) = (p %= q).

Lemma gcdp_map : forall p q, (gcdp p q)^f = gcdp p^f q^f.

Lemma fmorph_unity_root : forall n z, n.-unity_root (f z) = n.-unity_root z.

Lemma fmorph_primitive_root : forall n z,
  n.-primitive_root (f z) = n.-primitive_root z.

End MapFieldPoly.

Section MaxRoots.

Variable R : unitRingType.

Definition diff_roots (x y : R) := (x * y == y * x) && GRing.unit (y - x).

Fixpoint uniq_roots (rs : seq R) {struct rs} :=
  if rs is x :: rs' then all (diff_roots x) rs' && uniq_roots rs' else true.

Lemma uniq_roots_dvdp : forall p rs,
  all (root p) rs -> uniq_roots rs -> \prod_(z <- rs) ('X - z%:P) %| p.

Theorem max_ring_poly_roots : forall (p : {poly R}) rs,
  p != 0 -> all (root p) rs -> uniq_roots rs -> size rs < size p.

End MaxRoots.

Section FieldRoots.

Variable F : fieldType.
Implicit Type p : {poly F}.
Implicit Type rs : seq F.

Lemma uniq_rootsE : forall rs, uniq_roots rs = uniq rs.

Theorem max_poly_roots : forall p rs,
  p != 0 -> all (root p) rs -> uniq rs -> size rs < size p.

Variable n : nat.

Lemma max_unity_roots : forall rs,
  n > 0 -> all n.-unity_root rs -> uniq rs -> size rs <= n.

Lemma mem_unity_roots : forall rs,
    n > 0 -> all n.-unity_root rs -> uniq rs -> size rs = n ->
  n.-unity_root =i rs.

 Showing the existence of a primitive root requires the theory in cyclic. 

Variable z : F.
Hypothesis prim_z : n.-primitive_root z.

Lemma prod_factors_of_unity : \prod_(0 <= i < n) ('X - (z ^+ i)%:P) = 'X^n - 1.

Lemma prim_rootP : forall x, x ^+ n = 1 -> {i : 'I_n | x = z ^+ i}.

End FieldRoots.

Section MapPolyRoots.

Variables (F : fieldType) (R : unitRingType) (f : {rmorphism F -> R}).

Lemma map_diff_roots : forall x y, diff_roots (f x) (f y) = (x != y).

Lemma map_uniq_roots : forall s, uniq_roots (map f s) = uniq s.

End MapPolyRoots.

Section Deriv.

Variable R : ringType.

Implicit Types p q : {poly R}.

Definition deriv p := \poly_(i < (size p).-1) (p`_i.+1 *+ i.+1).

Notation "a ^` ()" := (deriv a).

Lemma coef_deriv : forall p i, p^`()`_i = p`_i.+1 *+ i.+1.

Lemma derivC : forall c, c%:P^`() = 0.

Lemma derivX : ('X)^`() = 1.

Lemma derivXn : forall n, 'X^n^`() = 'X^n.-1 *+ n.

Lemma deriv_linear_proof : linear deriv.

Canonical Structure deriv_linear := Linear deriv_linear_proof.

Lemma deriv0 : 0^`() = 0.

Lemma derivD : {morph deriv : p q / p + q}.

Lemma derivM : forall p q, (p * q)^`() = p^`() * q + p * q^`().

Lemma derivMn : forall n p, (p *+ n)^`() = p^`() *+ n.

Lemma derivMNn : forall n p, (p *- n)^`() = p^`() *- n.

Lemma derivN : {morph deriv : p / - p}.

Lemma derivZ : scalable deriv.

Lemma deriv_amulX : forall p c, (p * 'X + c%:P)^`() = p + p^`() * 'X.

Definition derivE := (derivC, derivX, deriv_amulX, derivM, derivD,
  derivMn, derivN, derivXn).

Definition derivn n p := iter n deriv p.

Notation "a ^` ( n )" := (derivn n a).

Lemma derivn0 : forall p, p^`(0) = p.

Lemma derivn1 : forall p, p^`(1) = p^`().

Lemma derivnS : forall p n, p^`(n.+1) = p^`(n)^`().

Lemma derivSn : forall p n, p^`(n.+1) = p^`()^`(n).

Lemma coef_derivn : forall n p i, p^`(n)`_i = p`_(n + i) *+ (n + i) ^_ n.

Lemma derivnC : forall c n, c%:P^`(n) = if n == 0%N then c%:P else 0.

Lemma derivn_linear_proof : forall n, linear (derivn n).

Canonical Structure derivn_linear n := Linear (derivn_linear_proof n).

Lemma derivnD : forall n, {morph (derivn n) : p q / p + q}.

Lemma derivnMn : forall n m p, (p *+ m)^`(n) = p^`(n) *+ m.

Lemma derivnMNn : forall n m p, (p *- m)^`(n) = p^`(n) *- m.

Lemma derivnN : forall n, {morph (derivn n) : p / - p}.

Lemma derivnZ : forall n, scalable (derivn n).

Lemma derivnXn : forall m n, 'X^m^`(n) = 'X^(m - n) *+ m ^_ n.

Lemma derivn_amulX : forall n p c,
 (p * 'X + c%:P)^`(n.+1) = p^`(n) *+ n.+1 + p^`(n.+1) * 'X.

Lemma derivn_poly0 : forall p n, size p <= n -> p^`(n) = 0.

 A normalising version of derivation to get the division by n! in Taylor 

Definition nderivn n p := \poly_(i < size p - n) (p`_(n + i) *+ 'C(n + i, n)).

Notation "a ^`N ( n )" := (nderivn n a).

Lemma coef_nderivn : forall n p i, p^`N(n)`_i = p`_(n + i) *+ 'C(n + i, n).

 Here is the division by n! 
Lemma nderivn_def : forall n p, p^`(n) = p^`N(n) *+ n`!.

Lemma nderivn0 : forall p, p^`N(0) = p.

Lemma nderivn1 : forall p, p^`N(1) = p^`().

Lemma nderivnC : forall c n, c%:P^`N(n) = if n == 0%N then c%:P else 0.

Lemma nderivnXn : forall m n, 'X^m^`N(n) = 'X^(m - n) *+ 'C(m, n).

Lemma nderivn_linear_proof : forall n, linear (nderivn n).

Canonical Structure nderivn_linear n := Linear (nderivn_linear_proof n).

Lemma nderivnD : forall n, {morph (nderivn n) : p q / p + q}.

Lemma nderivnMn : forall n m p, (p *+ m)^`N(n) = p^`N(n) *+ m.

Lemma nderivnMNn : forall n m p, (p *- m)^`N(n) = p^`N(n) *- m.

Lemma nderivnN : forall n, {morph (nderivn n) : p / - p}.

Lemma nderivnZ : forall n, scalable (nderivn n).

Lemma nderivn_amulX : forall n p c,
  (p * 'X + c%:P)^`N(n.+1) = p^`N(n) + p^`N(n.+1) * 'X.

Lemma nderivn_poly0 : forall p n, size p <= n -> p^`N(n) = 0.

Lemma nderiv_taylor : forall p x h,
  GRing.comm x h -> p.[x + h] = \sum_(i < size p) p^`N(i).[x] * h ^+ i.

Lemma nderiv_taylor_wide : forall n p x h,
    GRing.comm x h -> size p <= n ->
  p.[x + h] = \sum_(i < n) p^`N(i).[x] * h ^+ i.

End Deriv.

Notation "a ^` ()" := (deriv a) : ring_scope.
Notation "a ^` ( n )" := (derivn n a) : ring_scope.
Notation "a ^`N ( n )" := (nderivn n a) : ring_scope.

Lemma deriv_map : forall (R S : ringType) (f : {rmorphism R -> S}) p,
  (map_poly f p)^`() = map_poly f (p^`()).

Lemma derivn_map : forall (R S : ringType) (f : {rmorphism R -> S}) (n : nat) p,
  (map_poly f p)^`(n) = map_poly f (p^`(n)).

Lemma nderivn_map : forall (R S : ringType) (f : {rmorphism R -> S}) (n : nat) p,
  (map_poly f p)^`N(n) = map_poly f (p^`N(n)).

Section DerivC.

Variable R : comRingType.

Lemma derivPn : forall n (p: {poly R}), (p ^+ n.+1)^`() = p ^+ n * p^`() *+ n.+1.

Definition derivCE := (derivE, derivPn).

End DerivC.

Section PolyCompose.

Variable R: ringType.

Implicit Types p q : {poly R}.

Definition poly_comp q p := (map_poly polyC p).[q].

Local Notation "p \Po q" := (poly_comp q p) (at level 50).

Lemma poly_compE: forall p q, p \Po q = \sum_(i < size p) p`_i *: q^+i.

Lemma poly_comp0 : forall p, p \Po 0 = (p`_0)%:P.

Lemma poly_compC : forall c p, c%:P \Po p = c%:P.

Lemma poly_comp_is_additive : forall p, additive (poly_comp p).

Canonical Structure poly_comp_additive p := Additive (poly_comp_is_additive p).

Lemma poly_comp_is_linear : forall p, linear (poly_comp p).

Canonical Structure poly_comp_linear p := Linear (poly_comp_is_linear p).

Lemma poly_com0p : forall p, 0 \Po p = 0.

Lemma poly_comp_addl : forall p q r, (p + q) \Po r = (p \Po r) + (q \Po r).

Lemma poly_comp_subl : forall p q r, (p - q) \Po r = (p \Po r) - (q \Po r).

Lemma poly_comp_scall : forall c p q, (c *: p) \Po q = c *: (p \Po q).

Lemma poly_compX: forall p, p \Po 'X = p.

Lemma poly_comXp: forall p, 'X \Po p = p.

Lemma poly_comp_translateK : forall z, ('X + z%:P) \Po ('X - z%:P) = 'X.

Lemma poly_comp_amulX: forall c p q, (p * 'X + c%:P) \Po q = (p \Po q) * q + c%:P.

End PolyCompose.

Notation "p \Po q" := (poly_comp q p) (at level 50).

Section ComPolyCompose.

Variable R: comRingType.

Implicit Types p q r : {poly R}.

Lemma poly_comp_rmorphr : forall p, rmorphism (poly_comp p).

Canonical Structure poly_comp_rmorphism p := RMorphism (poly_comp_rmorphr p).

Lemma poly_comp_mull : forall p q r, (p * q) \Po r = (p \Po r) * (q \Po r).

Lemma horner_poly_comp : forall p q x, (p \Po q).[x] = p.[q.[x]].

Lemma poly_compA : forall p q r, (p \Po q) \Po r = p \Po (q \Po r).

Lemma deriv_poly_comp: forall p q, (p \Po q) ^`() = (p ^`() \Po q) * q^`().

End ComPolyCompose.

Module UnityRootTheory.

Notation "n .-unity_root" := (root_of_unity n) : unity_root_scope.
Notation "n .-primitive_root" := (primitive_root_of_unity n) : unity_root_scope.
Open Scope unity_root_scope.

Definition unity_rootE := unity_rootE.
Definition unity_rootP := @unity_rootP.
Implicit Arguments unity_rootP [R n z].

Definition prim_order_exists := prim_order_exists.
Notation prim_order_gt0 := prim_order_gt0.
Notation prim_expr_order := prim_expr_order.
Definition prim_expr_mod := prim_expr_mod.
Definition prim_order_dvd := prim_order_dvd.
Definition eq_prim_root_expr := eq_prim_root_expr.

Definition rmorph_unity_root := rmorph_unity_root.
Definition fmorph_unity_root := fmorph_unity_root.
Definition fmorph_primitive_root := fmorph_primitive_root.
Definition max_unity_roots := max_unity_roots.
Definition mem_unity_roots := mem_unity_roots.
Definition prim_rootP := prim_rootP.

End UnityRootTheory.