+ +

Library mathcomp.algebra.polydiv

+ +

+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+

+ +

+ 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.
+ +
+CoInductive 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.
+ +
+CoInductive 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 MonicDivisor.
+ +
+Variable R : ringType.
+Implicit Types p q r : {poly R }.
+ +
+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 rdivp_addl q r :
+  rdvdp d q → rdivp (q + r) d = rdivp q d + rdivp r d.
+ +
+Lemma rdivp_addr 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 rmodp_add 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.
+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 }.
+ +
+CoInductive 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.
+ +
+CoInductive 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.
+ +
+Hint Resolve lc_expn_scalp_neq0.
+ +
+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.
+ +
+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.
+ +
+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.
+ +
+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.
+ +
+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.
+ +
+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 dvdp_scaler c m n : c != 0 → m %| c *: n = (m %| n ).
+ +
+Lemma dvdp_scalel c m n : c != 0 → (c *: m %| n ) = (m %| n ).
+ +
+Lemma dvdp_opp 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_modr m n : gcdp m (n %% m) %= gcdp m n.
+ +
+Lemma gcdp_modl m n : gcdp (m %% n) n %= 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 coprimep_scalel c m n :
+  c != 0 → coprimep (c *: m) n = coprimep m n.
+ +
+Lemma coprimep_scaler 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 coprimep_mulr p q r : coprimep p (q × r) = (coprimep p q && coprimep p r ).
+ +
+Lemma coprimep_mull 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).
+ +
+CoInductive 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 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.
+ +
+Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp.
+Hint Resolve dvdp0.
+ +
+End CommonIdomain.
+ +
+Module Idomain.
+ +
+Include IdomainDefs.
+Export IdomainDefs.
+Include WeakIdomain.
+Include CommonIdomain.
+ +
+End Idomain.
+ +
+Module IdomainMonic.
+ +
+Import Ring ComRing UnitRing IdomainDefs Idomain.
+ +
+Section MonicDivisor.
+ +
+Variable R : idomainType.
+Variable q : {poly R }.
+Hypothesis monq : q \is monic.
+ +
+Implicit Type p d r : {poly R }.
+ +
+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.
+ +
+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 modp_scalel c p : (c *: p ) %% d = c *: (p %% d ).
+ +
+Lemma divp_scalel 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 modp_opp p : (- p ) %% d = - (p %% d ).
+ +
+Lemma divp_opp p : (- p ) %/ d = - (p %/ d ).
+ +
+Lemma modp_add p q : (p + q ) %% d = p %% d + q %% d.
+ +
+Lemma divp_add 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 modp_scaler c p : c \in GRing.unit → p %% (c *: d ) = (p %% d ).
+ +
+Lemma divp_scaler 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 modp_scalel 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 divp_scalel c p q : (c *: p ) %/ q = c *: (p %/ q ).
+ +
+Lemma modp_scaler c p d : c != 0 → p %% (c *: d ) = (p %% d ).
+ +
+Lemma divp_scaler 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 modp_opp p q : (- p ) %% q = - (p %% q ).
+ +
+Lemma divp_opp p q : (- p ) %/ q = - (p %/ q ).
+ +
+Lemma modp_add d p q : (p + q ) %% d = p %% d + q %% d.
+ +
+Lemma modNp p q : (- p ) %% q = - (p %% q ).
+ +
+Lemma divp_add d p q : (p + q ) %/ d = p %/ d + q %/ d.
+ +
+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.
+ +
+CoInductive 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.
+