Library mathcomp.algebra.polydiv

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop ssralg poly.

This file provides a library for the basic theory of Euclidean and pseudo- Euclidean division for polynomials over ring structures. The library defines two versions of the pseudo-euclidean division: one for coefficients in a (not necessarily commutative) ring structure and one for coefficients equipped with a structure of integral domain. From the latter we derive the definition of the usual Euclidean division for coefficients in a field. Only the definition of the pseudo-division for coefficients in an integral domain is exported by default and benefits from notations. Also, the only theory exported by default is the one of division for polynomials with coefficients in a field. Other definitions and facts are qualified using name spaces indicating the hypotheses made on the structure of coefficients and the properties of the polynomial one divides with.
Pdiv.Field (exported by the present library): edivp p q == pseudo-division of p by q with p q : {poly R} where R is an idomainType. Computes (k, quo, rem) : nat * {poly r} * {poly R}, such that size rem < size q and: + if lead_coef q is not a unit, then: (lead_coef q ^+ k) *: p = q * quo + rem + else if lead_coef q is a unit, then: p = q * quo + rem and k = 0 p %/ q == quotient (second component) computed by (edivp p q). p %% q == remainder (third component) computed by (edivp p q). scalp p q == exponent (first component) computed by (edivp p q). p %| q == tests the nullity of the remainder of the pseudo-division of p by q. rgcdp p q == Pseudo-greater common divisor obtained by performing the Euclidean algorithm on p and q using redivp as Euclidean division. p %= q == p and q are associate polynomials, i.e., p %| q and q %| p, or equivalently, p = c *: q for some nonzero constant c. gcdp p q == Pseudo-greater common divisor obtained by performing the Euclidean algorithm on p and q using edivp as Euclidean division. egcdp p q == The pair of Bezout coefficients: if e := egcdp p q, then size e.1 <= size q, size e.2 <= size p, and gcdp p q %= e.1 * p + e.2 * q coprimep p q == p and q are coprime, i.e., (gcdp p q) is a nonzero constant. gdcop q p == greatest divisor of p which is coprime to q. irreducible_poly p <-> p has only trivial (constant) divisors.
Pdiv.Idomain: theory available for edivp and the related operation under the sole assumption that the ring of coefficients is canonically an integral domain (R : idomainType).
Pdiv.IdomainMonic: theory available for edivp and the related operations under the assumption that the ring of coefficients is canonically and integral domain (R : idomainType) an the divisor is monic.
Pdiv.IdomainUnit: theory available for edivp and the related operations under the assumption that the ring of coefficients is canonically an integral domain (R : idomainType) and the leading coefficient of the divisor is a unit.
Pdiv.ClosedField: theory available for edivp and the related operation under the sole assumption that the ring of coefficients is canonically an algebraically closed field (R : closedField).
Pdiv.Ring : redivp p q == pseudo-division of p by q with p q : {poly R} where R is a ringType. Computes (k, quo, rem) : nat * {poly r} * {poly R}, such that if rem = 0 then quo * q = p * (lead_coef q ^+ k)
rdivp p q == quotient (second component) computed by (redivp p q). rmodp p q == remainder (third component) computed by (redivp p q). rscalp p q == exponent (first component) computed by (redivp p q). rdvdp p q == tests the nullity of the remainder of the pseudo-division of p by q. rgcdp p q == analogue of gcdp for coefficients in a ringType. rgdcop p q == analogue of gdcop for coefficients in a ringType. rcoprimep p q == analogue of coprimep p q for coefficients in a ringType.
Pdiv.RingComRreg : theory of the operations defined in Pdiv.Ring, when the ring of coefficients is canonically commutative (R : comRingType) and the leading coefficient of the divisor is both right regular and commutes as a constant polynomial with the divisor itself
Pdiv.RingMonic : theory of the operations defined in Pdiv.Ring, under the assumption that the divisor is monic.
Pdiv.UnitRing: theory of the operations defined in Pdiv.Ring, when the ring R of coefficients is canonically with units (R : unitRingType).

Set Implicit Arguments.

Import GRing.Theory.
Local Open Scope ring_scope.

Reserved Notation "p %= q" (at level 70, no associativity).


Module Pdiv.

Module CommonRing.

Section RingPseudoDivision.

Variable R : ringType.
Implicit Types d p q r : {poly R}.

Pseudo division, defined on an arbitrary ring
Definition redivp_rec (q : {poly R}) :=
  let sq := size q in
  let cq := lead_coef q in
   fix loop (k : nat) (qq r : {poly R})(n : nat) {struct n} :=
    if size r < sq then (k, qq, r) else
    let m := (lead_coef r) *: '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 k.+1 qq1 r1 n1 else (k.+1, qq1, r1).

Definition redivp_expanded_def p q :=
   if q == 0 then (0%N, 0, p) else redivp_rec q 0 0 p (size p).
Fact redivp_key : unit.
Definition redivp : {poly R} → {poly R} → nat × {poly R} × {poly R} :=
  locked_with redivp_key redivp_expanded_def.
Canonical redivp_unlockable := [unlockable fun redivp].

Definition rdivp p q := ((redivp p q).1).2.
Definition rmodp p q := (redivp p q).2.
Definition rscalp p q := ((redivp p q).1).1.
Definition rdvdp p q := rmodp q p == 0.
Definition rmultp := [rel m d | rdvdp d m].
Lemma redivp_def p q : redivp p q = (rscalp p q, rdivp p q, rmodp p q).

Lemma rdiv0p p : rdivp 0 p = 0.

Lemma rdivp0 p : rdivp p 0 = 0.

Lemma rdivp_small p q : size p < size q → rdivp p q = 0.

Lemma leq_rdivp p q : size (rdivp p q) ≤ size p.

Lemma rmod0p p : rmodp 0 p = 0.

Lemma rmodp0 p : rmodp p 0 = p.

Lemma rscalp_small p q : size p < size q → rscalp p q = 0%N.

Lemma ltn_rmodp p q : (size (rmodp p q) < size q) = (q != 0).

Lemma ltn_rmodpN0 p q : q != 0 → size (rmodp p q) < size q.

Lemma rmodp1 p : rmodp p 1 = 0.

Lemma rmodp_small p q : size p < size q → rmodp p q = p.

Lemma leq_rmodp m d : size (rmodp m d) ≤ size m.

Lemma rmodpC p c : c != 0 → rmodp p c%:P = 0.

Lemma rdvdp0 d : rdvdp d 0.

Lemma rdvd0p n : rdvdp 0 n = (n == 0).

Lemma rdvd0pP n : reflect (n = 0) (rdvdp 0 n).

Lemma rdvdpN0 p q : rdvdp p q → q != 0 → p != 0.

Lemma rdvdp1 d : rdvdp d 1 = (size d == 1%N).

Lemma rdvd1p m : rdvdp 1 m.

Lemma Nrdvdp_small (n d : {poly R}) :
  n != 0 → size n < size d → rdvdp d n = false.

Lemma rmodp_eq0P p q : reflect (rmodp p q = 0) (rdvdp q p).

Lemma rmodp_eq0 p q : rdvdp q p → rmodp p q = 0.

Lemma rdvdp_leq p q : rdvdp p q → q != 0 → size p ≤ size q.

Definition rgcdp 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 := rmodp 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 rgcd0p : left_id 0 rgcdp.

Lemma rgcdp0 : right_id 0 rgcdp.

Lemma rgcdpE p q :
  rgcdp p q = if size p < size q
    then rgcdp (rmodp q p) p else rgcdp (rmodp p q) q.

Variant comm_redivp_spec m d : nat × {poly R} × {poly R} → Type :=
  ComEdivnSpec 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) : comm_redivp_spec m d (k, q, r).

Lemma comm_redivpP m d : comm_redivp_spec m d (redivp m d).

Lemma rmodpp p : GRing.comm p (lead_coef p)%:P → rmodp p p = 0.

Definition rcoprimep (p q : {poly R}) := size (rgcdp p q) == 1%N.

Fixpoint rgdcop_rec q p n :=
  if n is m.+1 then
      if rcoprimep p q then p
        else rgdcop_rec q (rdivp p (rgcdp p q)) m
    else (q == 0)%:R.

Definition rgdcop q p := rgdcop_rec q p (size p).

Lemma rgdcop0 q : rgdcop q 0 = (q == 0)%:R.

End RingPseudoDivision.

End CommonRing.

Module RingComRreg.

Import CommonRing.

Section ComRegDivisor.

Variable R : ringType.
Variable d : {poly R}.
Hypothesis Cdl : GRing.comm d (lead_coef d)%:P.
Hypothesis Rreg : GRing.rreg (lead_coef d).

Implicit Types p q r : {poly R}.

Lemma redivp_eq q r :
    size r < size d →
    let k := (redivp (q × d + r) d).1.1 in
    let c := (lead_coef d ^+ k)%:P in
  redivp (q × d + r) d = (k, q × c, r × c).

this is a bad name
Lemma rdivp_eq p :
  p × (lead_coef d ^+ (rscalp p d))%:P = (rdivp p d) × d + (rmodp p d).

section variables impose an inconvenient order on parameters
Lemma eq_rdvdp k q1 p:
  p × ((lead_coef d)^+ k)%:P = q1 × d → rdvdp d p.

Variant rdvdp_spec p q : {poly R} → bool → Type :=
  | Rdvdp k q1 & p × ((lead_coef q)^+ k)%:P = q1 × q : rdvdp_spec p q 0 true
  | RdvdpN & rmodp p q != 0 : rdvdp_spec p q (rmodp p q) false.

Is that version useable ?

Lemma rdvdp_eqP p : rdvdp_spec p d (rmodp p d) (rdvdp d p).

Lemma rdvdp_mull p : rdvdp d (p × d).

Lemma rmodp_mull p : rmodp (p × d) d = 0.

Lemma rmodpp : rmodp d d = 0.

Lemma rdivpp : rdivp d d = (lead_coef d ^+ rscalp d d)%:P.

Lemma rdvdpp : rdvdp d d.

Lemma rdivpK p : rdvdp d p →
  rdivp p d × d = p × (lead_coef d ^+ rscalp p d)%:P.

End ComRegDivisor.

End RingComRreg.

Module RingMonic.

Import CommonRing.

Import RingComRreg.

Section RingMonic.

Variable R : ringType.
Implicit Types p q r : {poly R}.

Section MonicDivisor.

Variable d : {poly R}.
Hypothesis mond : d \is monic.

Lemma redivp_eq q r : size r < size d →
  let k := (redivp (q × d + r) d).1.1 in
  redivp (q × d + r) d = (k, q, r).

Lemma rdivp_eq p : p = rdivp p d × d + rmodp p d.

Lemma rdivpp : rdivp d d = 1.

Lemma rdivp_addl_mul_small q r : size r < size d → rdivp (q × d + r) d = q.

Lemma rdivp_addl_mul q r : rdivp (q × d + r) d = q + rdivp r d.

Lemma rdivpDl q r : rdvdp d q → rdivp (q + r) d = rdivp q d + rdivp r d.

Lemma rdivpDr q r : rdvdp d r → rdivp (q + r) d = rdivp q d + rdivp r d.

Lemma rdivp_mull p : rdivp (p × d) d = p.

Lemma rmodp_mull p : rmodp (p × d) d = 0.

Lemma rmodpp : rmodp d d = 0.

Lemma rmodp_addl_mul_small q r : size r < size d → rmodp (q × d + r) d = r.

Lemma rmodpD p q : rmodp (p + q) d = rmodp p d + rmodp q d.

Lemma rmodp_mulmr p q : rmodp (p × (rmodp q d)) d = rmodp (p × q) d.

Lemma rdvdpp : rdvdp d d.

section variables impose an inconvenient order on parameters
Lemma eq_rdvdp q1 p : p = q1 × d → rdvdp d p.

Lemma rdvdp_mull p : rdvdp d (p × d).

Lemma rdvdpP p : reflect (∃ qq, p = qq × d) (rdvdp d p).

Lemma rdivpK p : rdvdp d p → (rdivp p d) × d = p.

End MonicDivisor.

Lemma drop_poly_rdivp n p : drop_poly n p = rdivp p 'X^n.

Lemma take_poly_rmodp n p : take_poly n p = rmodp p 'X^n.

End RingMonic.

End RingMonic.

Module Ring.

Include CommonRing.
Import RingMonic.

Section ExtraMonicDivisor.

Variable R : ringType.

Implicit Types d p q r : {poly R}.

Lemma rdivp1 p : rdivp p 1 = p.

Lemma rdvdp_XsubCl p x : rdvdp ('X - x%:P) p = root p x.

Lemma polyXsubCP p x : reflect (p.[x] = 0) (rdvdp ('X - x%:P) p).

Lemma root_factor_theorem p x : root p x = (rdvdp ('X - x%:P) p).

End ExtraMonicDivisor.

End Ring.

Module ComRing.

Import Ring.

Import RingComRreg.

Section CommutativeRingPseudoDivision.

Variable R : comRingType.

Implicit Types d p q m n r : {poly R}.

Variant redivp_spec (m d : {poly R}) : nat × {poly R} × {poly R} → Type :=
  EdivnSpec k (q r: {poly R}) of
    (lead_coef d ^+ k) *: m = q × d + r &
   (d != 0 → size r < size d) : redivp_spec m d (k, q, r).

Lemma redivpP m d : redivp_spec m d (redivp m d).

Lemma rdivp_eq d p :
  (lead_coef d ^+ rscalp p d) *: p = rdivp p d × d + rmodp p d.

Lemma rdvdp_eqP d p : rdvdp_spec p d (rmodp p d) (rdvdp d p).

Lemma rdvdp_eq q p :
  rdvdp q p = (lead_coef q ^+ rscalp p q *: p == rdivp p q × q).

End CommutativeRingPseudoDivision.

End ComRing.

Module UnitRing.

Import Ring.

Section UnitRingPseudoDivision.

Variable R : unitRingType.
Implicit Type p q r d : {poly R}.

Lemma uniq_roots_rdvdp p rs :
  all (root p) rs → uniq_roots rs → rdvdp (\prod_(z <- rs) ('X - z%:P)) p.

End UnitRingPseudoDivision.

End UnitRing.

Module IdomainDefs.

Import Ring.

Section IDomainPseudoDivisionDefs.

Variable R : idomainType.
Implicit Type p q r d : {poly R}.

Definition edivp_expanded_def p q :=
  let: (k, d, r) as edvpq := redivp p q in
  if lead_coef q \in GRing.unit then
    (0%N, (lead_coef q)^-k *: d, (lead_coef q)^-k *: r)
  else edvpq.
Fact edivp_key : unit.
Definition edivp := locked_with edivp_key edivp_expanded_def.
Canonical edivp_unlockable := [unlockable fun edivp].

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.
Definition eqp p q := (dvdp p q) && (dvdp q p).

End IDomainPseudoDivisionDefs.

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.
End IdomainDefs.

Module WeakIdomain.

Import Ring ComRing UnitRing IdomainDefs.

Section WeakTheoryForIDomainPseudoDivision.

Variable R : idomainType.
Implicit Type p q r d : {poly R}.

Lemma edivp_def p q : edivp p q = (scalp p q, divp p q, modp p q).

Lemma edivp_redivp p q : lead_coef q \in GRing.unit = false →
  edivp p q = redivp p q.

Lemma divpE p q :
  p %/ q = if lead_coef q \in GRing.unit
    then lead_coef q ^- rscalp p q *: rdivp p q
    else rdivp p q.

Lemma modpE p q :
  p %% q = if lead_coef q \in GRing.unit
    then lead_coef q ^- rscalp p q *: (rmodp p q)
    else rmodp p q.

Lemma scalpE p q :
  scalp p q = if lead_coef q \in GRing.unit then 0%N else rscalp p q.

Lemma dvdpE p q : p %| q = rdvdp p q.

Lemma lc_expn_scalp_neq0 p q : lead_coef q ^+ scalp p q != 0.

Hint Resolve lc_expn_scalp_neq0 : core.

Variant edivp_spec (m d : {poly R}) :
                                     nat × {poly R} × {poly R} → bool → Type :=
|Redivp_spec k (q r: {poly R}) of
  (lead_coef d ^+ k) *: m = q × d + r & lead_coef d \notin GRing.unit &
  (d != 0 → size r < size d) : edivp_spec m d (k, q, r) false
|Fedivp_spec (q r: {poly R}) of m = q × d + r & (lead_coef d \in GRing.unit) &
  (d != 0 → size r < size d) : edivp_spec m d (0%N, q, r) true.

There are several ways to state this fact. The most appropriate statement might be polished in light of usage.
Lemma edivpP m d : edivp_spec m d (edivp m d) (lead_coef d \in GRing.unit).

Lemma edivp_eq d q r : size r < size d → lead_coef d \in GRing.unit →
  edivp (q × d + r) d = (0%N, q, r).

Lemma divp_eq p q : (lead_coef q ^+ scalp p q) *: p = (p %/ q) × q + (p %% q).

Lemma dvdp_eq q p : (q %| p) = (lead_coef q ^+ scalp p q *: p == (p %/ q) × q).

Lemma divpK d p : d %| p → p %/ d × d = (lead_coef d ^+ scalp p d) *: p.

Lemma divpKC d p : d %| p → d × (p %/ d) = (lead_coef d ^+ scalp p d) *: p.

Lemma dvdpP q p :
  reflect (exists2 cqq, cqq.1 != 0 & cqq.1 *: p = cqq.2 × q) (q %| p).

Lemma mulpK p q : q != 0 → p × q %/ q = lead_coef q ^+ scalp (p × q) q *: p.

Lemma mulKp p q : q != 0 → q × p %/ q = lead_coef q ^+ scalp (p × q) q *: p.

Lemma divpp p : p != 0 → p %/ p = (lead_coef p ^+ scalp p p)%:P.

End WeakTheoryForIDomainPseudoDivision.

#[global] Hint Resolve lc_expn_scalp_neq0 : core.

End WeakIdomain.

Module CommonIdomain.

Import Ring ComRing UnitRing IdomainDefs WeakIdomain.

Section IDomainPseudoDivision.

Variable R : idomainType.
Implicit Type p q r d m n : {poly R}.

Lemma scalp0 p : scalp p 0 = 0%N.

Lemma divp_small p q : size p < size q → p %/ q = 0.

Lemma leq_divp p q : (size (p %/ q) ≤ size p).

Lemma div0p p : 0 %/ p = 0.

Lemma divp0 p : p %/ 0 = 0.

Lemma divp1 m : m %/ 1 = m.

Lemma modp0 p : p %% 0 = p.

Lemma mod0p p : 0 %% p = 0.

Lemma modp1 p : p %% 1 = 0.

Hint Resolve divp0 divp1 mod0p modp0 modp1 : core.

Lemma modp_small p q : size p < size q → p %% q = p.

Lemma modpC p c : c != 0 → p %% c%:P = 0.

Lemma modp_mull p q : (p × q) %% q = 0.

Lemma modp_mulr d p : (d × p) %% d = 0.

Lemma modpp d : d %% d = 0.

Lemma ltn_modp p q : (size (p %% q) < size q) = (q != 0).

Lemma ltn_divpl d q p : d != 0 →
   (size (q %/ d) < size p) = (size q < size (p × d)).

Lemma leq_divpr d p q : d != 0 →
   (size p ≤ size (q %/ d)) = (size (p × d) ≤ size q).

Lemma divpN0 d p : d != 0 → (p %/ d != 0) = (size d ≤ size p).

Lemma size_divp p q : q != 0 → size (p %/ q) = (size p - (size q).-1)%N.

Lemma ltn_modpN0 p q : q != 0 → size (p %% q) < size q.

Lemma modp_mod p q : (p %% q) %% q = p %% q.

Lemma leq_modp m d : size (m %% d) ≤ size m.

Lemma dvdp0 d : d %| 0.

Hint Resolve dvdp0 : core.

Lemma dvd0p p : (0 %| p) = (p == 0).

Lemma dvd0pP p : reflect (p = 0) (0 %| p).

Lemma dvdpN0 p q : p %| q → q != 0 → p != 0.

Lemma dvdp1 d : (d %| 1) = (size d == 1%N).

Lemma dvd1p m : 1 %| m.

Lemma gtNdvdp p q : p != 0 → size p < size q → (q %| p) = false.

Lemma modp_eq0P p q : reflect (p %% q = 0) (q %| p).

Lemma modp_eq0 p q : (q %| p) → p %% q = 0.

Lemma leq_divpl d p q :
  d %| p → (size (p %/ d) ≤ size q) = (size p ≤ size (q × d)).

Lemma dvdp_leq p q : q != 0 → p %| q → size p ≤ size q.

Lemma eq_dvdp c quo q p : c != 0 → c *: p = quo × q → q %| p.

Lemma dvdpp d : d %| d.

Hint Resolve dvdpp : core.

Lemma divp_dvd p q : p %| q → (q %/ p) %| q.

Lemma dvdp_mull m d n : d %| n → d %| m × n.

Lemma dvdp_mulr n d m : d %| m → d %| m × n.

Hint Resolve dvdp_mull dvdp_mulr : core.

Lemma dvdp_mul d1 d2 m1 m2 : d1 %| m1 → d2 %| m2 → d1 × d2 %| m1 × m2.

Lemma dvdp_addr m d n : d %| m → (d %| m + n) = (d %| n).

Lemma dvdp_addl n d m : d %| n → (d %| m + n) = (d %| m).

Lemma dvdp_add d m n : d %| m → d %| n → d %| m + n.

Lemma dvdp_add_eq d m n : d %| m + n → (d %| m) = (d %| n).

Lemma dvdp_subr d m n : d %| m → (d %| m - n) = (d %| n).

Lemma dvdp_subl d m n : d %| n → (d %| m - n) = (d %| m).

Lemma dvdp_sub d m n : d %| m → d %| n → d %| m - n.

Lemma dvdp_mod d n m : d %| n → (d %| m) = (d %| m %% n).

Lemma dvdp_trans : transitive (@dvdp R).

Lemma dvdp_mulIl p q : p %| p × q.

Lemma dvdp_mulIr p q : q %| p × q.

Lemma dvdp_mul2r r p q : r != 0 → (p × r %| q × r) = (p %| q).

Lemma dvdp_mul2l r p q: r != 0 → (r × p %| r × q) = (p %| q).

Lemma ltn_divpr d p q :
  d %| q → (size p < size (q %/ d)) = (size (p × d) < size q).

Lemma dvdp_exp d k p : 0 < k → d %| p → d %| (p ^+ k).

Lemma dvdp_exp2l d k l : k ≤ l → d ^+ k %| d ^+ l.

Lemma dvdp_Pexp2l d k l : 1 < size d → (d ^+ k %| d ^+ l) = (k ≤ l).

Lemma dvdp_exp2r p q k : p %| q → p ^+ k %| q ^+ k.

Lemma dvdp_exp_sub p q k l: p != 0 →
  (p ^+ k %| q × p ^+ l) = (p ^+ (k - l) %| q).

Lemma dvdp_XsubCl p x : ('X - x%:P) %| p = root p x.

Lemma polyXsubCP p x : reflect (p.[x] = 0) (('X - x%:P) %| p).

Lemma eqp_div_XsubC p c :
  (p == (p %/ ('X - c%:P)) × ('X - c%:P)) = ('X - c%:P %| p).

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

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

Lemma root_bigmul x (ps : seq {poly R}) :
  ~~root (\big[*%R/1]_(p <- ps) p) x = all (fun p ⇒ ~~ root p x) ps.

Lemma eqpP m n :
  reflect (exists2 c12, (c12.1 != 0) && (c12.2 != 0) & c12.1 *: m = c12.2 *: n)
          (m %= n).

Lemma eqp_eq p q: p %= q → (lead_coef q) *: p = (lead_coef p) *: q.

Lemma eqpxx : reflexive (@eqp R).

Hint Resolve eqpxx : core.

Lemma eqp_sym : symmetric (@eqp R).

Lemma eqp_trans : transitive (@eqp R).

Lemma eqp_ltrans : left_transitive (@eqp R).

Lemma eqp_rtrans : right_transitive (@eqp R).

Lemma eqp0 p : (p %= 0) = (p == 0).

Lemma eqp01 : 0 %= (1 : {poly R}) = false.

Lemma eqp_scale p c : c != 0 → c *: p %= p.

Lemma eqp_size p q : p %= q → size p = size q.

Lemma size_poly_eq1 p : (size p == 1%N) = (p %= 1).

Lemma polyXsubC_eqp1 (x : R) : ('X - x%:P %= 1) = false.

Lemma dvdp_eqp1 p q : p %| q → q %= 1 → p %= 1.

Lemma eqp_dvdr q p d: p %= q → d %| p = (d %| q).

Lemma eqp_dvdl d2 d1 p : d1 %= d2 → d1 %| p = (d2 %| p).

Lemma dvdpZr c m n : c != 0 → m %| c *: n = (m %| n).

Lemma dvdpZl c m n : c != 0 → (c *: m %| n) = (m %| n).

Lemma dvdpNl d p : (- d) %| p = (d %| p).

Lemma dvdpNr d p : d %| (- p) = (d %| p).

Lemma eqp_mul2r r p q : r != 0 → (p × r %= q × r) = (p %= q).

Lemma eqp_mul2l r p q: r != 0 → (r × p %= r × q) = (p %= q).

Lemma eqp_mull r p q: q %= r → p × q %= p × r.

Lemma eqp_mulr q p r : p %= q → p × r %= q × r.

Lemma eqp_exp p q k : p %= q → p ^+ k %= q ^+ k.

Lemma polyC_eqp1 (c : R) : (c%:P %= 1) = (c != 0).

Lemma dvdUp d p: d %= 1 → d %| p.

Lemma dvdp_size_eqp p q : p %| q → size p == size q = (p %= q).

Lemma eqp_root p q : p %= q → root p =1 root q.

Lemma eqp_rmod_mod p q : rmodp p q %= modp p q.

Lemma eqp_rdiv_div p q : rdivp p q %= divp p q.

Lemma dvd_eqp_divl d p q (dvd_dp : d %| q) (eq_pq : p %= q) :
  p %/ d %= q %/ d.

Definition gcdp_rec 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 := modp 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.

Definition gcdp := nosimpl gcdp_rec.

Lemma gcd0p : left_id 0 gcdp.

Lemma gcdp0 : right_id 0 gcdp.

Lemma gcdpE p q :
  gcdp p q = if size p < size q
    then gcdp (modp q p) p else gcdp (modp p q) q.

Lemma size_gcd1p p : size (gcdp 1 p) = 1%N.

Lemma size_gcdp1 p : size (gcdp p 1) = 1%N.

Lemma gcdpp : idempotent gcdp.

Lemma dvdp_gcdlr p q : (gcdp p q %| p) && (gcdp p q %| q).

Lemma dvdp_gcdl p q : gcdp p q %| p.

Lemma dvdp_gcdr p q :gcdp p q %| q.

Lemma leq_gcdpl p q : p != 0 → size (gcdp p q) ≤ size p.

Lemma leq_gcdpr p q : q != 0 → size (gcdp p q) ≤ size q.

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

Lemma gcdpC p q : gcdp p q %= gcdp q p.

Lemma gcd1p p : gcdp 1 p %= 1.

Lemma gcdp1 p : gcdp p 1 %= 1.

Lemma gcdp_addl_mul p q r: gcdp r (p × r + q) %= gcdp r q.

Lemma gcdp_addl m n : gcdp m (m + n) %= gcdp m n.

Lemma gcdp_addr m n : gcdp m (n + m) %= gcdp m n.

Lemma gcdp_mull m n : gcdp n (m × n) %= n.

Lemma gcdp_mulr m n : gcdp n (n × m) %= n.

Lemma gcdp_scalel c m n : c != 0 → gcdp (c *: m) n %= gcdp m n.

Lemma gcdp_scaler c m n : c != 0 → gcdp m (c *: n) %= gcdp m n.

Lemma dvdp_gcd_idl m n : m %| n → gcdp m n %= m.

Lemma dvdp_gcd_idr m n : n %| m → gcdp m n %= n.

Lemma gcdp_exp p k l : gcdp (p ^+ k) (p ^+ l) %= p ^+ minn k l.

Lemma gcdp_eq0 p q : gcdp p q == 0 = (p == 0) && (q == 0).

Lemma eqp_gcdr p q r : q %= r → gcdp p q %= gcdp p r.

Lemma eqp_gcdl r p q : p %= q → gcdp p r %= gcdp q r.

Lemma eqp_gcd p1 p2 q1 q2 : p1 %= p2 → q1 %= q2 → gcdp p1 q1 %= gcdp p2 q2.

Lemma eqp_rgcd_gcd p q : rgcdp p q %= gcdp p q.

Lemma gcdp_modl m n : gcdp (m %% n) n %= gcdp m n.

Lemma gcdp_modr m n : gcdp m (n %% m) %= gcdp m n.

Lemma gcdp_def d m n :
    d %| m → d %| n → (∀ d', d' %| m → d' %| n → d' %| d) →
  gcdp m n %= d.

Definition coprimep p q := size (gcdp p q) == 1%N.

Lemma coprimep_size_gcd p q : coprimep p q → size (gcdp p q) = 1%N.

Lemma coprimep_def p q : coprimep p q = (size (gcdp p q) == 1%N).

Lemma coprimepZl c m n : c != 0 → coprimep (c *: m) n = coprimep m n.

Lemma coprimepZr c m n: c != 0 → coprimep m (c *: n) = coprimep m n.

Lemma coprimepp p : coprimep p p = (size p == 1%N).

Lemma gcdp_eqp1 p q : gcdp p q %= 1 = coprimep p q.

Lemma coprimep_sym p q : coprimep p q = coprimep q p.

Lemma coprime1p p : coprimep 1 p.

Lemma coprimep1 p : coprimep p 1.

Lemma coprimep0 p : coprimep p 0 = (p %= 1).

Lemma coprime0p p : coprimep 0 p = (p %= 1).

This is different from coprimeP in div. shall we keep this?
Lemma coprimepP p q :
 reflect (∀ d, d %| p → d %| q → d %= 1) (coprimep p q).

Lemma coprimepPn p q : p != 0 →
  reflect (∃ d, (d %| gcdp p q) && ~~ (d %= 1)) (~~ coprimep p q).

Lemma coprimep_dvdl q p r : r %| q → coprimep p q → coprimep p r.

Lemma coprimep_dvdr p q r : r %| p → coprimep p q → coprimep r q.

Lemma coprimep_modl p q : coprimep (p %% q) q = coprimep p q.

Lemma coprimep_modr q p : coprimep q (p %% q) = coprimep q p.

Lemma rcoprimep_coprimep q p : rcoprimep q p = coprimep q p.

Lemma eqp_coprimepr p q r : q %= r → coprimep p q = coprimep p r.

Lemma eqp_coprimepl p q r : q %= r → coprimep q p = coprimep r p.

This should be implemented with an extended remainder sequence
Fixpoint egcdp_rec p q k {struct k} : {poly R} × {poly R} :=
  if k is k'.+1 then
    if q == 0 then (1, 0) else
    let: (u, v) := egcdp_rec q (p %% q) k' in
      (lead_coef q ^+ scalp p q *: v, (u - v × (p %/ q)))
  else (1, 0).

Definition egcdp p q :=
  if size q ≤ size p then egcdp_rec p q (size q)
    else let e := egcdp_rec q p (size p) in (e.2, e.1).

No provable egcd0p
Lemma egcdp0 p : egcdp p 0 = (1, 0).

Lemma egcdp_recP : ∀ k p q, q != 0 → size q ≤ k → size q ≤ size p →
  let e := (egcdp_rec p q k) in
    [/\ size e.1 ≤ size q, size e.2 ≤ size p & gcdp p q %= e.1 × p + e.2 × q].

Lemma egcdpP p q : p != 0 → q != 0 → ∀ (e := egcdp p q),
  [/\ size e.1 ≤ size q, size e.2 ≤ size p & gcdp p q %= e.1 × p + e.2 × q].

Lemma egcdpE p q (e := egcdp p q) : gcdp p q %= e.1 × p + e.2 × q.

Lemma Bezoutp p q : ∃ u, u.1 × p + u.2 × q %= (gcdp p q).

Lemma Bezout_coprimepP p q :
  reflect (∃ u, u.1 × p + u.2 × q %= 1) (coprimep p q).

Lemma coprimep_root p q x : coprimep p q → root p x → q.[x] != 0.

Lemma Gauss_dvdpl p q d: coprimep d q → (d %| p × q) = (d %| p).

Lemma Gauss_dvdpr p q d: coprimep d q → (d %| q × p) = (d %| p).

This could be simplified with the introduction of lcmp
Lemma Gauss_dvdp m n p : coprimep m n → (m × n %| p) = (m %| p) && (n %| p).

Lemma Gauss_gcdpr p m n : coprimep p m → gcdp p (m × n) %= gcdp p n.

Lemma Gauss_gcdpl p m n : coprimep p n → gcdp p (m × n) %= gcdp p m.

Lemma coprimepMr p q r : coprimep p (q × r) = (coprimep p q && coprimep p r).

Lemma coprimepMl p q r: coprimep (q × r) p = (coprimep q p && coprimep r p).

Lemma modp_coprime k u n : k != 0 → (k × u) %% n %= 1 → coprimep k n.

Lemma coprimep_pexpl k m n : 0 < k → coprimep (m ^+ k) n = coprimep m n.

Lemma coprimep_pexpr k m n : 0 < k → coprimep m (n ^+ k) = coprimep m n.

Lemma coprimep_expl k m n : coprimep m n → coprimep (m ^+ k) n.

Lemma coprimep_expr k m n : coprimep m n → coprimep m (n ^+ k).

Lemma gcdp_mul2l p q r : gcdp (p × q) (p × r) %= (p × gcdp q r).

Lemma gcdp_mul2r q r p : gcdp (q × p) (r × p) %= gcdp q r × p.

Lemma mulp_gcdr p q r : r × (gcdp p q) %= gcdp (r × p) (r × q).

Lemma mulp_gcdl p q r : (gcdp p q) × r %= gcdp (p × r) (q × r).

Lemma coprimep_div_gcd p q : (p != 0) || (q != 0) →
  coprimep (p %/ (gcdp p q)) (q %/ gcdp p q).

Lemma divp_eq0 p q : (p %/ q == 0) = [|| p == 0, q ==0 | size p < size q].

Lemma dvdp_div_eq0 p q : q %| p → (p %/ q == 0) = (p == 0).

Lemma Bezout_coprimepPn p q : p != 0 → q != 0 →
  reflect (exists2 uv : {poly R} × {poly R},
    (0 < size uv.1 < size q) && (0 < size uv.2 < size p) &
      uv.1 × p = uv.2 × q)
    (~~ (coprimep p q)).

Lemma dvdp_pexp2r m n k : k > 0 → (m ^+ k %| n ^+ k) = (m %| n).

Lemma root_gcd p q x : root (gcdp p q) x = root p x && root q x.

Lemma root_biggcd x (ps : seq {poly R}) :
  root (\big[gcdp/0]_(p <- ps) p) x = all (fun p ⇒ root p x) ps.

"gdcop Q P" is the Greatest Divisor of P which is coprime to Q if P null, we pose that gdcop returns 1 if Q null, 0 otherwise
Fixpoint gdcop_rec q p k :=
  if k is m.+1 then
      if coprimep p q then p
        else gdcop_rec q (divp p (gcdp p q)) m
    else (q == 0)%:R.

Definition gdcop q p := gdcop_rec q p (size p).

Variant gdcop_spec q p : {poly R} → Type :=
  GdcopSpec r of (dvdp r p) & ((coprimep r q) || (p == 0))
  & (∀ d, dvdp d p → coprimep d q → dvdp d r)
  : gdcop_spec q p r.

Lemma gdcop0 q : gdcop q 0 = (q == 0)%:R.

Lemma gdcop_recP q p k : size p ≤ k → gdcop_spec q p (gdcop_rec q p k).

Lemma gdcopP q p : gdcop_spec q p (gdcop q p).

Lemma coprimep_gdco p q : (q != 0)%B → coprimep (gdcop p q) p.

Lemma size2_dvdp_gdco p q d : p != 0 → size d = 2%N →
  (d %| (gdcop q p)) = (d %| p) && ~~(d %| q).

Lemma dvdp_gdco p q : (gdcop p q) %| q.

Lemma root_gdco p q x : p != 0 → root (gdcop q p) x = root p x && ~~(root q x).

Lemma dvdp_comp_poly r p q : (p %| q) → (p \Po r) %| (q \Po r).

Lemma gcdp_comp_poly r p q : gcdp p q \Po r %= gcdp (p \Po r) (q \Po r).

Lemma coprimep_comp_poly r p q : coprimep p q → coprimep (p \Po r) (q \Po r).

Lemma coprimep_addl_mul p q r : coprimep r (p × r + q) = coprimep r q.

Definition irreducible_poly p :=
  (size p > 1) × (∀ q, size q != 1%N → q %| p → q %= p) : Prop.

Lemma irredp_neq0 p : irreducible_poly p → p != 0.

Definition apply_irredp p (irr_p : irreducible_poly p) := irr_p.2.
Coercion apply_irredp : irreducible_poly >-> Funclass.

Lemma modp_XsubC p c : p %% ('X - c%:P) = p.[c]%:P.

Lemma coprimep_XsubC p c : coprimep p ('X - c%:P) = ~~ root p c.

Lemma coprimep_XsubC2 (a b : R) : b - a != 0 →
  coprimep ('X - a%:P) ('X - b%:P).

Lemma coprimepX p : coprimep p 'X = ~~ root p 0.

Lemma eqp_monic : {in monic &, ∀ p q, (p %= q) = (p == q)}.

Lemma dvdp_mul_XsubC p q c :
  (p %| ('X - c%:P) × q) = ((if root p c then p %/ ('X - c%:P) else p) %| q).

Lemma dvdp_prod_XsubC (I : Type) (r : seq I) (F : I → R) p :
    p %| \prod_(i <- r) ('X - (F i)%:P) →
  {m | p %= \prod_(i <- mask m r) ('X - (F i)%:P)}.

Lemma irredp_XsubC (x : R) : irreducible_poly ('X - x%:P).

Lemma irredp_XsubCP d p :
  irreducible_poly p → d %| p → {d %= 1} + {d %= p}.

End IDomainPseudoDivision.

#[global] Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 : core.
#[global] Hint Resolve dvdp_mull dvdp_mulr dvdpp dvdp0 : core.

End CommonIdomain.

Module Idomain.

Include IdomainDefs.
Export IdomainDefs.
Include WeakIdomain.
Include CommonIdomain.

End Idomain.

Module IdomainMonic.

Import Ring ComRing UnitRing IdomainDefs Idomain.

Section IdomainMonic.

Variable R : idomainType.

Implicit Type p d r : {poly R}.

Section MonicDivisor.

Variable q : {poly R}.
Hypothesis monq : q \is monic.

Lemma divpE p : p %/ q = rdivp p q.

Lemma modpE p : p %% q = rmodp p q.

Lemma scalpE p : scalp p q = 0%N.

Lemma divp_eq p : p = (p %/ q) × q + (p %% q).

Lemma divpp p : q %/ q = 1.

Lemma dvdp_eq p : (q %| p) = (p == (p %/ q) × q).

Lemma dvdpP p : reflect (∃ qq, p = qq × q) (q %| p).

Lemma mulpK p : p × q %/ q = p.

Lemma mulKp p : q × p %/ q = p.

End MonicDivisor.

Lemma drop_poly_divp n p : drop_poly n p = p %/ 'X^n.

Lemma take_poly_modp n p : take_poly n p = p %% 'X^n.

End IdomainMonic.

End IdomainMonic.

Module IdomainUnit.

Import Ring ComRing UnitRing IdomainDefs Idomain.

Section UnitDivisor.

Variable R : idomainType.
Variable d : {poly R}.

Hypothesis ulcd : lead_coef d \in GRing.unit.

Implicit Type p q r : {poly R}.

Lemma divp_eq p : p = (p %/ d) × d + (p %% d).

Lemma edivpP p q r : p = q × d + r → size r < size d →
  q = (p %/ d) ∧ r = p %% d.

Lemma divpP p q r : p = q × d + r → size r < size d → q = (p %/ d).

Lemma modpP p q r : p = q × d + r → size r < size d → r = (p %% d).

Lemma ulc_eqpP p q : lead_coef q \is a GRing.unit →
  reflect (exists2 c : R, c != 0 & p = c *: q) (p %= q).

Lemma dvdp_eq p : (d %| p) = (p == p %/ d × d).

Lemma ucl_eqp_eq p q : lead_coef q \is a GRing.unit →
  p %= q → p = (lead_coef p / lead_coef q) *: q.

Lemma modpZl c p : (c *: p) %% d = c *: (p %% d).

Lemma divpZl c p : (c *: p) %/ d = c *: (p %/ d).

Lemma eqp_modpl p q : p %= q → (p %% d) %= (q %% d).

Lemma eqp_divl p q : p %= q → (p %/ d) %= (q %/ d).

Lemma modpN p : (- p) %% d = - (p %% d).

Lemma divpN p : (- p) %/ d = - (p %/ d).

Lemma modpD p q : (p + q) %% d = p %% d + q %% d.

Lemma divpD p q : (p + q) %/ d = p %/ d + q %/ d.

Lemma mulpK q : (q × d) %/ d = q.

Lemma mulKp q : (d × q) %/ d = q.

Lemma divp_addl_mul_small q r : size r < size d → (q × d + r) %/ d = q.

Lemma modp_addl_mul_small q r : size r < size d → (q × d + r) %% d = r.

Lemma divp_addl_mul q r : (q × d + r) %/ d = q + r %/ d.

Lemma divpp : d %/ d = 1.

Lemma leq_trunc_divp m : size (m %/ d × d) ≤ size m.

Lemma dvdpP p : reflect (∃ q, p = q × d) (d %| p).

Lemma divpK p : d %| p → p %/ d × d = p.

Lemma divpKC p : d %| p → d × (p %/ d) = p.

Lemma dvdp_eq_div p q : d %| p → (q == p %/ d) = (q × d == p).

Lemma dvdp_eq_mul p q : d %| p → (p == q × d) = (p %/ d == q).

Lemma divp_mulA p q : d %| q → p × (q %/ d) = p × q %/ d.

Lemma divp_mulAC m n : d %| m → m %/ d × n = m × n %/ d.

Lemma divp_mulCA p q : d %| p → d %| q → p × (q %/ d) = q × (p %/ d).

Lemma modp_mul p q : (p × (q %% d)) %% d = (p × q) %% d.

End UnitDivisor.

Section MoreUnitDivisor.

Variable R : idomainType.
Variable d : {poly R}.
Hypothesis ulcd : lead_coef d \in GRing.unit.

Implicit Types p q : {poly R}.

Lemma expp_sub m n : n ≤ m → (d ^+ (m - n))%N = d ^+ m %/ d ^+ n.

Lemma divp_pmul2l p q : lead_coef q \in GRing.unit → d × p %/ (d × q) = p %/ q.

Lemma divp_pmul2r p q : lead_coef p \in GRing.unit → q × d %/ (p × d) = q %/ p.

Lemma divp_divl r p q :
    lead_coef r \in GRing.unit → lead_coef p \in GRing.unit →
  q %/ p %/ r = q %/ (p × r).

Lemma divpAC p q : lead_coef p \in GRing.unit → q %/ d %/ p = q %/ p %/ d.

Lemma modpZr c p : c \in GRing.unit → p %% (c *: d) = (p %% d).

Lemma divpZr c p : c \in GRing.unit → p %/ (c *: d) = c^-1 *: (p %/ d).

End MoreUnitDivisor.

End IdomainUnit.

Module Field.

Import Ring ComRing UnitRing.
Include IdomainDefs.
Export IdomainDefs.
Include CommonIdomain.

Section FieldDivision.

Variable F : fieldType.

Implicit Type p q r d : {poly F}.

Lemma divp_eq p q : p = (p %/ q) × q + (p %% q).

Lemma divp_modpP p q d r : p = q × d + r → size r < size d →
  q = (p %/ d) ∧ r = p %% d.

Lemma divpP p q d r : p = q × d + r → size r < size d →
  q = (p %/ d).

Lemma modpP p q d r : p = q × d + r → size r < size d → r = (p %% d).

Lemma eqpfP p q : p %= q → p = (lead_coef p / lead_coef q) *: q.

Lemma dvdp_eq q p : (q %| p) = (p == p %/ q × q).

Lemma eqpf_eq p q : reflect (exists2 c, c != 0 & p = c *: q) (p %= q).

Lemma modpZl c p q : (c *: p) %% q = c *: (p %% q).

Lemma mulpK p q : q != 0 → p × q %/ q = p.

Lemma mulKp p q : q != 0 → q × p %/ q = p.

Lemma divpZl c p q : (c *: p) %/ q = c *: (p %/ q).

Lemma modpZr c p d : c != 0 → p %% (c *: d) = (p %% d).

Lemma divpZr c p d : c != 0 → p %/ (c *: d) = c^-1 *: (p %/ d).

Lemma eqp_modpl d p q : p %= q → (p %% d) %= (q %% d).

Lemma eqp_divl d p q : p %= q → (p %/ d) %= (q %/ d).

Lemma eqp_modpr d p q : p %= q → (d %% p) %= (d %% q).

Lemma eqp_mod p1 p2 q1 q2 : p1 %= p2 → q1 %= q2 → p1 %% q1 %= p2 %% q2.

Lemma eqp_divr (d m n : {poly F}) : m %= n → (d %/ m) %= (d %/ n).

Lemma eqp_div p1 p2 q1 q2 : p1 %= p2 → q1 %= q2 → p1 %/ q1 %= p2 %/ q2.

Lemma eqp_gdcor p q r : q %= r → gdcop p q %= gdcop p r.

Lemma eqp_gdcol p q r : q %= r → gdcop q p %= gdcop r p.

Lemma eqp_rgdco_gdco q p : rgdcop q p %= gdcop q p.

Lemma modpD d p q : (p + q) %% d = p %% d + q %% d.

Lemma modpN p q : (- p) %% q = - (p %% q).

Lemma modNp p q : (- p) %% q = - (p %% q).

Lemma divpD d p q : (p + q) %/ d = p %/ d + q %/ d.

Lemma divpN p q : (- p) %/ q = - (p %/ q).

Lemma divp_addl_mul_small d q r : size r < size d → (q × d + r) %/ d = q.

Lemma modp_addl_mul_small d q r : size r < size d → (q × d + r) %% d = r.

Lemma divp_addl_mul d q r : d != 0 → (q × d + r) %/ d = q + r %/ d.

Lemma divpp d : d != 0 → d %/ d = 1.

Lemma leq_trunc_divp d m : size (m %/ d × d) ≤ size m.

Lemma divpK d p : d %| p → p %/ d × d = p.

Lemma divpKC d p : d %| p → d × (p %/ d) = p.

Lemma dvdp_eq_div d p q : d != 0 → d %| p → (q == p %/ d) = (q × d == p).

Lemma dvdp_eq_mul d p q : d != 0 → d %| p → (p == q × d) = (p %/ d == q).

Lemma divp_mulA d p q : d %| q → p × (q %/ d) = p × q %/ d.

Lemma divp_mulAC d m n : d %| m → m %/ d × n = m × n %/ d.

Lemma divp_mulCA d p q : d %| p → d %| q → p × (q %/ d) = q × (p %/ d).

Lemma expp_sub d m n : d != 0 → m ≥ n → (d ^+ (m - n))%N = d ^+ m %/ d ^+ n.

Lemma divp_pmul2l d q p : d != 0 → q != 0 → d × p %/ (d × q) = p %/ q.

Lemma divp_pmul2r d p q : d != 0 → p != 0 → q × d %/ (p × d) = q %/ p.

Lemma divp_divl r p q : q %/ p %/ r = q %/ (p × r).

Lemma divpAC d p q : q %/ d %/ p = q %/ p %/ d.

Lemma edivp_def p q : edivp p q = (0%N, p %/ q, p %% q).

Lemma divpE p q : p %/ q = (lead_coef q)^-(rscalp p q) *: (rdivp p q).

Lemma modpE p q : p %% q = (lead_coef q)^-(rscalp p q) *: (rmodp p q).

Lemma scalpE p q : scalp p q = 0%N.

Just to have it without importing the weak theory
Lemma dvdpE p q : p %| q = rdvdp p q.

Variant edivp_spec m d : nat × {poly F} × {poly F} → Type :=
  EdivpSpec n q r of
  m = q × d + r & (d != 0) ==> (size r < size d) : edivp_spec m d (n, q, r).

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

Lemma edivp_eq d q r : size r < size d → edivp (q × d + r) d = (0%N, q, r).

Lemma modp_mul p q m : (p × (q %% m)) %% m = (p × q) %% m.

Lemma dvdpP p q : reflect (∃ qq, p = qq × q) (q %| p).

Lemma Bezout_eq1_coprimepP p q :
  reflect (∃ u, u.1 × p + u.2 × q = 1) (coprimep p q).

Lemma dvdp_gdcor p q : q != 0 → p %| (gdcop q p) × (q ^+ size p).

Lemma reducible_cubic_root p q :
  size p ≤ 4 → 1 < size q < size p → q %| p → {r | root p r}.

Lemma cubic_irreducible p :
  1 < size p ≤ 4 → (∀ x, ~~ root p x) → irreducible_poly p.

Section FieldRingMap.

Variable rR : ringType.

Variable f : {rmorphism F → rR}.

Implicit Type a b : {poly F}.

Lemma redivp_map a b :
  redivp a^f b^f = (rscalp a b, (rdivp a b)^f, (rmodp a b)^f).

End FieldRingMap.

Section FieldMap.

Variable rR : idomainType.

Variable f : {rmorphism F → rR}.

Implicit Type a b : {poly F}.

Lemma edivp_map a b :
  edivp a^f b^f = (0%N, (a %/ b)^f, (a %% b)^f).

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

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

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

Lemma egcdp_map p q :
  egcdp (map_poly f p) (map_poly f q)
     = (map_poly f (egcdp p q).1, map_poly f (egcdp p q).2).

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

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

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

Lemma coprimep_map p q : coprimep p^f q^f = coprimep p q.

Lemma gdcop_rec_map p q n : (gdcop_rec p q n)^f = gdcop_rec p^f q^f n.

Lemma gdcop_map p q : (gdcop p q)^f = gdcop p^f q^f.

End FieldMap.

End FieldDivision.

End Field.

Module ClosedField.

Import Field.

Section closed.

Variable F : closedFieldType.

Lemma root_coprimep (p q : {poly F}):
  (∀ x, root p x → q.[x] != 0) → coprimep p q.

Lemma coprimepP (p q : {poly F}):
  reflect (∀ x, root p x → q.[x] != 0) (coprimep p q).

End closed.

End ClosedField.

End Pdiv.

Export Pdiv.Field.