\import Algebra.Algebra
\import Algebra.Domain
\import Algebra.Domain.Bezout
\import Algebra.Domain.Euclidean
\import Algebra.Domain.GCD
\import Algebra.Field
\import Algebra.Group
\import Algebra.Group.Category
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Module.LinearMap
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Ordered
\import Algebra.Pointed
\import Algebra.Pointed.Category
\import Algebra.Ring
\import Algebra.Ring.Category
\import Algebra.Ring.RingHom
\import Algebra.Ring.Ideal
\import Algebra.Ring.QPoly
\import Algebra.Semiring
\import Arith.Nat
\import Category \hiding (Map,univalence)
\import Data.Array
\import Data.Or
\import Equiv
\import Equiv.Fiber
\import Equiv.Univalence
\import Function \hiding (id,o)
\import Function.Meta
\import HLevel
\import Logic
\import Logic.Meta
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\import Set.Countable
\import Set.Fin
\open Monoid \hiding (equals)

\data Poly (R : AddPointed)
  | pzero
  | padd (Poly R) R
  | peq : padd pzero  = pzero
  \where {
    \open QPoly

    \func toQPoly {R : AddPointed} (p : Poly R) : QPoly R \elim p
      | pzero => in~ nil
      | padd p e => qadd (toQPoly p) e
      | peq => path (~-equiv _ _ idp)

    \func fromArray {R : AddPointed} (l : Array R) : Poly R \elim l
      | nil => pzero
      | :: a l => padd (fromArray l) a

    \func cfunc {R : AddPointed} (l : Array R) : toQPoly (fromArray l) = in~ l \elim l
      | nil => idp
      | :: a l => pmap (qadd __ a) (cfunc l)

    \func path-lem {R : AddPointed} {p : R.zro = R.zro} : inv (path peq) *> pmap2 padd idp p *> path peq = idp
      => pmap (inv (path peq) *> pmap2 padd idp __ *> path peq) (prop-isProp _ idp) *> pmap (_ *>) (idp_*> _) *> inv_*> _

    \func toQPoly-nil {R : AddPointed} {p : Poly R} : toQPoly p = in~ nil -> p = pzero \elim p
      | pzero => \lam _ => idp
      | padd p e => \lam s => \have t => qadd_nil s \in pmap2 padd (toQPoly-nil t.) t. *> path peq
      | peq => pathOver $ coe_pi *> ext (\lam s => coe_path (path peq) _ idp *> path-lem)

    \func gfunc {R : AddPointed} (l : Array R) (p : Poly R) : toQPoly p = in~ l -> p = fromArray l \elim l, p
      | nil, pzero => \lam _ => idp
      | nil, padd p e => \lam s => pmap2 padd (toQPoly-nil (qadd_nil s).) (qadd_nil s). *> path peq
      | nil, peq => pathOver $ coe_pi *> ext (\lam _ => coe_path (path peq) _ idp *> path-lem)
      | :: a l, pzero => \lam s => inv (path peq) *> pmap2 padd (gfunc l pzero (nil_cons s).) (nil_cons s).
      | :: a l, padd p e => \lam s => pmap2 padd (gfunc l p (qadd_cons s).) (qadd_cons {_} {e} {a} {toQPoly p} {l} s).
      | :: a l, peq => pathOver $ coe_pi *> ext (\lam s => coe_path (path peq) _ idp *> pmap (inv (path peq) *>) (pmap2 (\lam x => pmap2 padd (gfunc l pzero x)) prop-pi set-pi))

    \lemma toQPoly-equiv {R : AddPointed} : Equiv (toQPoly {R})
      => contrFibers=>Equiv \case \elim __ \with {
        | in~ l => \new Contr {
          | center => (fromArray l, cfunc l)
          | contraction t => ext (inv (gfunc l t. t.))
        }
      }

    \use \level levelSet {R : AddPointed} : isSet (Poly R)
      => transportInv isSet (Equiv-to-= toQPoly-equiv) (\lam _ _ _ _ => set-pi)

    \func poly-countable {R : AddPointed} (c : Countable R) : Countable (Poly R)
      => surj-countable (quotient-countable (array-countable c)) (Equiv.isSurj {symQEquiv toQPoly-equiv})

    \lemma poly-trivial {R : AddPointed} (p : \Pi (x : R) -> x = zro) (p : Poly R) : p = pzero \elim p
      | pzero => idp
      | padd q e => pmap2 padd (poly-trivial p q) (p e) *> peq
  }

\func polyMap (f : AddPointedHom) (p : Poly f.Dom) : Poly f.Cod \elim p
  | pzero => pzero
  | padd p e => padd (polyMap f p) (f e)
  | peq => rewrite f.func-zro peq

\lemma polyMap-comp {A B C : AddPointed} (f : AddPointedHom A B) (g : AddPointedHom B C) {p : Poly A} : polyMap g (polyMap f p) = polyMap (g ∘ f) p \elim p
  | pzero => idp
  | padd p e => pmap (padd __ _) (polyMap-comp f g)

\lemma polyMap-inj {A B : AddPointed} {f : AddPointedHom A B} (inj : isInj f) {p q : Poly A} (s : polyMap f p = polyMap f q) : p = q \elim p, q
  | pzero, pzero => idp
  | pzero, padd q b => inv peq *> pmap2 padd (polyMap-inj {_} {_} {f} inj $ pmap polyShift s) (inj $ func-zro *> pmap (polyCoef __ ) s)
  | padd p a, pzero => pmap2 padd (polyMap-inj {_} {_} {f} inj $ pmap polyShift s) (inj $ pmap (polyCoef __ ) s *> inv func-zro) *> peq
  | padd p a, padd q b => pmap2 padd (later $ polyMap-inj {_} {_} {f} inj $ pmap polyShift s) (inj $ pmap (polyCoef __ ) s)

\lemma polyMap_fromArray {f : AddPointedHom} {l : Array f.Dom} : polyMap f (Poly.fromArray l) = Poly.fromArray (map f l) \elim l
  | nil => idp
  | a :: l => pmap (padd __ _) polyMap_fromArray

\func polyEval {R : Ring} (p : Poly R) (a : R) : R \elim p
  | pzero => 
  | padd p e => polyEval p a * a + e
  | peq => zro-right *> zro_*-left

\func polyMapEval {A : AddPointed} {R : Ring} (f : AddPointedHom A R) (p : Poly A) (a : R) : R
  => polyEval (polyMap f p) a

\lemma polyEval_polyMap {f : RingHom} {p : Poly f.Dom} {a : f.Dom} : polyEval (polyMap f p) (f a) = f (polyEval p a) \elim p
  | pzero => inv func-zro
  | padd p e => inv $ func-+ *> pmap (`+ _) (f.func-* *> pmap (`* _) (inv polyEval_polyMap))

\func polyCoef {R : AddPointed} (p : Poly R) (n : Nat) : R \elim p, n
  | pzero, _ => 
  | padd p e,  => e
  | padd p e, suc n => polyCoef p n
  | peq,  => idp
  | peq, suc n => idp

\lemma polyCoef=0 {R : AddPointed} {r : R} {n : Nat} (n>0 :  < n) : polyCoef (padd pzero r) n =  \elim n
  | suc n => idp

\lemma polyCoef_polyMap {f : AddPointedHom} {p : Poly f.Dom} {n : Nat} : polyCoef (polyMap f p) n = f (polyCoef p n) \elim p, n
  | pzero, n => inv f.func-zro
  | padd p e,  => idp
  | padd p e, suc n => polyCoef_polyMap

\lemma polyEval_fromArray {R : Ring} {l : Array R} {a : R} : polyEval (Poly.fromArray l) a = R.BigSum (\lam j => l j * pow a j) \elim l
  | nil => idp
  | c :: l => +-comm *> pmap2 (+) (inv ide-right) (pmap (`* a) polyEval_fromArray *> R.BigSum-rdistr *> pmap R.BigSum (exts \lam j => *-assoc))

\lemma polyMapEval_fromArray {R : AddPointed} {E : Ring} {f : AddPointedHom R E} {l : Array f.Dom} {a : f.Cod}
  : polyMapEval f (Poly.fromArray l) a = AddMonoid.BigSum (\lam j => f (l j) * pow a j)
  => pmap (polyEval __ a) polyMap_fromArray *> polyEval_fromArray

\lemma polyCoef_fromArray {R : AddPointed} {l : Array R} {j : Fin l.len} : polyCoef (Poly.fromArray l) j = l j \elim l, j
  | a :: l,  => idp
  | a :: l, suc j => polyCoef_fromArray

\func lastCoef {R : AddPointed} (p : Poly R) => polyCoef p 

\func polyShift {R : AddPointed} (p : Poly R) : Poly R \elim p
  | pzero => pzero
  | padd p e => p
  | peq => idp

\lemma poly-root-div {R : CRing} {p : Poly R} {a : R} (q : polyEval p a = )
  : LDiv a (polyCoef p ) (negative (polyEval (polyShift p) a)) \elim p
  | pzero => \new LDiv {
    | inv-right => simplify
  }
  | padd p e => \new LDiv {
    | inv-right => R.negative_*-right *> inv (AddGroup.fromZero $ +-comm *> pmap (`+ e) (R.negative-isInv *> *-comm) *> q)
  }

\lemma padd=pzero {R : AddPointed} {p : Poly R} {a : R} (q : padd p a = pzero) : \Sigma (p = pzero) (a = )
  => \have t => q *> inv peq
     \in (pmap polyShift t, pmap (polyCoef __ ) t)

\func monomial {R : AddPointed} (c : R) (n : Nat) : Poly R \elim n
  |  => padd pzero c
  | suc n => padd (monomial c n) 

\lemma polyCoef_monomial {R : AddPointed} {c : R} {n : Nat} : polyCoef (monomial c n) n = c \elim n
  |  => idp
  | suc n => polyCoef_monomial

\lemma polyMap_monomial {f : AddPointedHom} {c : f.Dom} {n : Nat} : polyMap f (monomial c n) = monomial (f c) n \elim n
  |  => idp
  | suc n => pmap2 padd polyMap_monomial func-zro

\lemma polyEval_monomial {R : Ring} {c a : R} {n : Nat} : polyEval (monomial c n) a = c * pow a n \elim n
  |  => simplify
  | suc n => rewrite polyEval_monomial equation

\lemma polyMapEval_monomial {f : RingHom} {a : f.Cod} {n : Nat} : polyMapEval f (monomial  n) a = pow a n
  => pmap (polyEval __ a) polyMap_monomial *> polyEval_monomial *> pmap (`* _) func-ide *> ide-left

\lemma monomial_zro {R : AddPointed} {n : Nat} : monomial R.zro n = pzero \elim n
  |  => peq
  | suc n => rewrite monomial_zro peq

\instance PolyRing (R : Ring) : Ring (Poly R)
  | zro => pzero
  | + (p q : Poly R) : Poly R \with {
    | pzero, q => q
    | padd p e, pzero => padd p e
    | padd p e, padd q e' => padd (p + q) (e R.+ e')
    | padd p e, peq => pmap2 padd zro-right R.zro-right
    | peq, pzero => path peq
    | peq, padd q e => pmap (padd q) R.zro-left
  }
  | zro-left => idp
  | zro-right {p : Poly R} : p + pzero = p \elim p {
    | pzero => idp
    | padd p e => idp
  }
  | +-assoc {p q s : Poly R} : (p + q) + s = p + (q + s) \elim p, q, s {
    | pzero, q, s => idp
    | padd p e, pzero, s => idp
    | padd p e, padd q e1, pzero => idp
    | padd p e, padd q e1, padd s e2 => pmap2 padd +-assoc R.+-assoc
  }
  | +-comm {p q : Poly R} : p + q = q + p \elim p, q {
    | pzero, pzero => idp
    | pzero, padd q e => idp
    | padd p e, pzero => idp
    | padd p e, padd q e' => pmap2 padd +-comm R.+-comm
  }
  | ide => padd pzero 
  | * (p q : Poly R) : Poly R \elim p {
    | pzero => pzero
    | padd p e => padd (p * q)  + e *c q
    | peq => pmap (_ +) zro_*c *> path peq
  }
  | ide-left => pmap2 (+) (path peq) ide_*c
  | ide-right {p : Poly R} : p * padd pzero  = p \elim p {
    | pzero => idp
    | padd p e => pmap2 padd (zro-right *> ide-right) equation
  }
  | *-assoc {p q s : Poly R} : (p * q) * s = p * (q * s) \elim p {
    | pzero => idp
    | padd p e => rdistr *> +-assoc *> pmap2 (padd __  +) *-assoc (pmap2 (+) zro_*c (inv *c-comm-left))
  }
  | ldistr {p q s : Poly R} : p * (q + s) = p * q + p * s \elim p {
    | pzero => idp
    | padd p e => pmap2 (+) (pmap2 padd ldistr (inv R.zro-left)) *c-ldistr
        *> +-assoc *> pmap (_ +) (inv +-assoc *> pmap (`+ _) +-comm *> +-assoc) *> inv +-assoc
  }
  | rdistr {p q s : Poly R} : (p + q) * s = p * s + q * s \elim p, q, s {
    | pzero, q, s => idp
    | padd p e, pzero, s => inv zro-right
    | padd p e, padd q e', s => pmap2 (+) (pmap2 padd rdistr (inv R.zro-left)) *c-rdistr
        *> +-assoc *> pmap (_ +) (inv +-assoc *> pmap (`+ _) +-comm *> +-assoc) *> inv +-assoc
  }
  | negative (p : Poly R) : Poly R \with {
    | pzero => pzero
    | padd p e => padd (negative p) (R.negative e)
    | peq => pmap (padd pzero) R.negative_zro *> path peq
  }
  | negative-left {p : Poly R} : negative p + p = pzero \elim p {
    | pzero => idp
    | padd p e => pmap2 padd negative-left R.negative-left *> path peq
  }
  | natCoef n => padd pzero (R.natCoef n)
  | natCoefZero => pmap (padd pzero) R.natCoefZero *> peq
  | natCoefSuc n => pmap (padd pzero) (R.natCoefSuc n)
  \where {
    \func \infixl  *c {R : Ring} (r : R) (p : Poly R) : Poly R \elim p
      | pzero => pzero
      | padd p e => padd (r *c p) (r R.* e)
      | peq => pmap (padd pzero) R.zro_*-right *> path peq

    \lemma zro_*c {R : Ring} {p : Poly R} :  *c p = pzero \elim p
      | pzero => idp
      | padd p e => pmap2 padd zro_*c R.zro_*-left *> path peq

    \lemma ide_*c {R : Ring} {p : Poly R} :  *c p = p \elim p
      | pzero => idp
      | padd p e => pmap2 padd ide_*c R.ide-left

    \lemma *c-rdistr {R : Ring} {e r : R} {p : Poly R} : (e R.+ r) *c p = e *c p + r *c p \elim p
      | pzero => idp
      | padd p e1 => pmap2 padd *c-rdistr R.rdistr

    \lemma *c-ldistr {R : Ring} {c : R} {p q : Poly R} : c *c (p + q) = c *c p + c *c q \elim p, q
      | pzero, q => idp
      | padd p e, pzero => idp
      | padd p e, padd q e' => pmap2 padd *c-ldistr R.ldistr

    \lemma *c-assoc {R : Ring} {c e : R} {p : Poly R} : c R.* e *c p = c *c (e *c p) \elim p
      | pzero => idp
      | padd p e' => pmap2 padd *c-assoc R.*-assoc

    \lemma *c-comm-left {R : Ring} {r : R} {p q : Poly R} : r *c (p * q) = (r *c p) * q \elim p
      | pzero => idp
      | padd p e => *c-ldistr *> pmap2 (+) (pmap2 padd *c-comm-left R.zro_*-right) (inv *c-assoc)

    \lemma padd0_*-comm {R : Ring} {p q : Poly R} : p * padd q  = padd (p * q)  \elim p
      | pzero => inv (path peq)
      | padd p e => pmap2 (\lam x => padd (x + _)) padd0_*-comm equation

    \lemma *c_* {R : Ring} {c : R} {p : Poly R} : c *c p = padd pzero c * p
      => inv $ pmap (`+ _) peq

    \lemma *c_negative {R : Ring} {c : R} {p : Poly R} : c *c negative p = negative (c *c p) \elim p
      | pzero => idp
      | padd p e => pmap2 padd *c_negative R.negative_*-right
  }

\lemma padd-expand {R : Ring} {p : Poly R} {e : R} : padd p e = p * padd   + padd  e \elim p
  | pzero => idp
  | padd p a => pmap2 padd (padd-expand *> simplify simplify) simplify

\func polyHom {R : Ring} : RingHom R (PolyRing R) \cowith
  | func => padd pzero
  | func-+ => idp
  | func-ide => idp
  | func-* => pmap (padd pzero) (inv zro-left)

\lemma polyHom_polyMapEval {R : Ring} {p : Poly R} : polyMapEval polyHom p (padd  ) = p \elim p
  | pzero => idp
  | padd p e => unfold polyMapEval $ rewrite polyHom_polyMapEval $ inv padd-expand

\lemma factorHom_polyMapEval {R : CRing} {I : Ideal (PolyAlgebra R)} {p : Poly R} : polyMapEval (factorHom {I} ∘ polyHom) p (in~ (padd  )) = in~ p
  => pmap (polyEval __ _) (inv (polyMap-comp _ _)) *> polyEval_polyMap *> pmap factorHom polyHom_polyMapEval

\instance PolyAlgebra (R : CRing) : CAlgebra R
  | Ring => PolyRing R
  | *c => *c
  | *c-assoc => *c-assoc
  | *c-ldistr => *c-ldistr
  | *c-rdistr => *c-rdistr
  | ide_*c => ide_*c
  | *c-comm-left => *c-comm-left
  | *-comm {p q : Poly R} : p * q = q * p \elim p, q {
    | pzero, pzero => idp
    | pzero, padd q e => inv (path peq) *> pmap (padd __ ) *-comm
    | padd p e, pzero => pmap (padd __ ) *-comm *> path peq
    | padd p e, padd q e' => pmap2 (\lam x y => padd x ( R.+ y)) (pmap (`+ _) *-comm *> +-assoc *> pmap2 (padd __  +) (inv *-comm) +-comm *> inv +-assoc *> pmap (`+ _) *-comm) R.*-comm
  }
  \where \open PolyRing

\instance PolyRingWith# (R : Ring.With#) : Ring.With#
  | Ring => PolyRing R
  | #0 (p : Poly R) : \Prop \with {
    | pzero => Empty
    | padd p e => #0 p || R.#0 e
    | peq => ext (||.rec' absurd R.#0-zro, absurd)
  }
  | #0-zro => absurd
  | #0-+ {p q : Poly R} (h : #0 (p + q)) : #0 p || #0 q \elim p, q, h {
    | pzero, q, h => byRight h
    | padd p e, pzero, h => byLeft h
    | padd p e, padd q e', byLeft h => ||.map byLeft byLeft (#0-+ h)
    | padd p e, padd q e', byRight h => ||.map byRight byRight (R.#0-+ h)
  }
  | #0-tight {p : Poly R} (h : Not (#0 p)) : p = pzero \elim p {
    | pzero => idp
    | padd p e => pmap2 padd (#0-tight (\lam x => h (byLeft x))) (R.#0-tight (\lam x => h (byRight x))) *> path peq
  }
  | #0-*-left {p q : Poly R} (h : #0 (p * q)) : #0 p \elim p {
    | pzero => h
    | padd p e => ||.rec' (||.map #0-*-left (\lam x => absurd (R.#0-zro x))) (\lam x => byRight (#0_*c-left x)) (#0-+ h)
  }
  | #0-*-right {p q : Poly R} (h : #0 (p * q)) : #0 q \elim p {
    | pzero => absurd h
    | padd p e => ||.rec' (||.rec' #0-*-right (\lam x => absurd (R.#0-zro x))) #0_*c-right (#0-+ h)
  }
  \where {
    \open PolyRing

    \lemma #0_*c-left {R : Ring.With#} {e : R} {p : Poly R} (h : #0 (e *c p)) : R.#0 e \elim p, h
      | padd p e', byLeft h => #0_*c-left h
      | padd p e', byRight h => R.#0-*-left h

    \lemma #0_*c-right {R : Ring.With#} {e : R} {p : Poly R} (h : #0 (e *c p)) : #0 p \elim p, h
      | padd p e', byLeft h => byLeft (#0_*c-right h)
      | padd p e', byRight h => byRight (R.#0-*-right h)
  }

\instance PolyCRingWith# (R : CRing.With#) : CRing.With#
  | Ring.With# => PolyRingWith# R
  | *-comm => PolyAlgebra.*-comm

\instance PolyDomain (R : Domain) : Domain
  | Ring.With# => PolyRingWith# R
  | zro#ide => byRight R.zro#ide
  | #0-* {p q : Poly R} (p#0 : #0 p) (q#0 : #0 q) : #0 (p * q) \elim p, q {
    | pzero, _ => absurd p#0
    | _, pzero => absurd q#0
    | padd p e, padd q e' => rewrite R.zro-left $ assuming
        (\lam h => ||.rec' (\lam q#0' => \case AddGroup.With#.#0-+-left {PolyRingWith# R} (#0-* {R} {padd p e} p#0 q#0') \with {
          | byLeft x => \have t : padd (p * q)  + p * padd pzero e' = p * padd q e' => pmap (`+ _) (inv padd0_*-comm) *> inv ldistr *> pmap2 (p * padd __ __) zro-right R.zro-left
                        \in byLeft $ transport #0 (+-assoc *> pmap (_ +) +-comm *> inv +-assoc *> pmap (`+ _) t) x
          | byRight x => h $ ||.rec' absurd (\lam x => x) (#0-*-right x)
        }) h q#0)
        \lam e'#0 => assuming (\lam h => ||.rec' (\lam p#0' => \case AddGroup.With#.#0-+-left {PolyRingWith# R} (#0-* p#0' q#0) \with {
          | byLeft x => byLeft x
          | byRight x => h (#0_*c-left x)
        }) h p#0) \lam e#0 => byRight (R.#0-* e#0 e'#0)
  }
  \where {
    \open PolyRing
    \open PolyRingWith#
  }

\instance PolyIntegralDomain (R : IntegralDomain) : IntegralDomain
  | Domain => PolyDomain R
  | *-comm => PolyAlgebra.*-comm

\instance PolyStrictDomain (R : StrictDomain) : StrictDomain
  | Ring => PolyRing R
  | zro/=ide x => R.zro/=ide (pmap lastCoef x)
  | zeroProduct {p q : Poly R} (pq=0 : p * q = pzero) : (p = pzero) || (q = pzero) \elim p, q {
    | pzero, _ => byLeft idp
    | _, pzero => byRight idp
    | padd p e, padd q e' => \case R.zeroProduct $ inv R.zro-left *> pmap lastCoef pq=0 \with {
      | byLeft e=0 => \case zeroProduct $ inv (pmap (_ +) zro_*c *> zro-right) *> (rewrite e=0 in pmap polyShift pq=0) \with {
        | byLeft p=0 => byLeft (pmap2 padd p=0 e=0 *> path peq)
        | byRight x => byRight x
      }
      | byRight e'=0 => \case zeroProduct {R} {padd p e} $ rewrite (e'=0, padd0_*-comm) in pmap polyShift pq=0 \with {
        | byLeft x => byLeft x
        | byRight q=0 => byRight (pmap2 padd q=0 e'=0 *> path peq)
      }
    }
  }
  \where \open PolyRing

\instance PolyStrictIntegralDomain (R : StrictIntegralDomain) : StrictIntegralDomain
  | StrictDomain => PolyStrictDomain R
  | *-comm => PolyAlgebra.*-comm

\instance PolyDecRing (R : Ring.Dec) : Ring.Dec
  | Ring => PolyRing R
  | decideEq (p q : Poly R) : Dec (p = q) \with {
    | pzero, pzero => yes idp
    | pzero, padd q a => \case decideEq pzero q, R.decideEq  a \with {
      | yes e1, yes e2 => yes (inv peq *> pmap2 padd e1 e2)
      | _, no n => no (\lam e => n (pmap lastCoef e))
      | no n, _ => no (\lam e => n (pmap polyShift e))
    }
    | padd p a, pzero => \case decideEq p pzero, R.decideEq a  \with {
      | yes e1, yes e2 => yes (pmap2 padd e1 e2 *> path peq)
      | _, no n => no (\lam e => n (pmap lastCoef e))
      | no n, _ => no (\lam e => n (pmap polyShift e))
    }
    | padd p a, padd q a' => \case decideEq p q, R.decideEq a a' \with {
      | yes e1, yes e2 => yes (pmap2 padd e1 e2)
      | _, no n => no (\lam e => n (pmap lastCoef e))
      | no n, _ => no (\lam e => n (pmap polyShift e))
    }
  }

\lemma polyCoef_+ {R : Ring} {p q : Poly R} {n : Nat} : polyCoef (p + q) n = polyCoef p n + polyCoef q n \elim p, q, n
  | pzero, q, n => rewrite zro-left (inv zro-left)
  | padd p x, padd q y,  => idp
  | padd p x, pzero, n => inv zro-right
  | padd p x, padd q y, suc n => polyCoef_+

\lemma polyCoef_BigSum {R : Ring} {l : Array (Poly R)} {n : Nat} : polyCoef (AddMonoid.BigSum l) n = AddMonoid.BigSum (map (polyCoef __ n) l) \elim l
  | nil => idp
  | a :: l => polyCoef_+ *> pmap (_ +) polyCoef_BigSum

\func polyCoefHom {R : Ring} {n : Nat} : AddGroupHom (PolyRing R) R \cowith
  | func => polyCoef __ n
  | func-zro => idp
  | func-+ => polyCoef_+

\lemma polyCoef_negative {R : Ring} {p : Poly R} {n : Nat} : polyCoef (negative p) n = negative (polyCoef p n)
  => polyCoefHom.func-negative

\lemma polyCoef_*c {R : Ring} {a : R} {p : Poly R} {n : Nat} : polyCoef (a PolyRing.*c p) n = a * polyCoef p n \elim p, n
  | pzero, n => inv zro_*-right
  | padd p e,  => idp
  | padd p e, suc n => polyCoef_*c

\lemma polyCoef_*-right {R : Ring} {a : R} {p : Poly R} {n : Nat} : polyCoef (p * padd pzero a) n = polyCoef p n * a \elim p, n
  | pzero, n => inv zro_*-left
  | padd p e,  => zro-left
  | padd p e, suc n => rewrite (zro-right {PolyRing R}) polyCoef_*-right

\lemma polyCoef_* {R : Ring} {a : R} {p : Poly R} {k n : Nat} : polyCoef (monomial a k * p) (k + n) = a * polyCoef p n \elim k
  |  => pmap (\lam s => polyCoef (s + _) n) peq *> rewrite zro-left polyCoef_*c
  | suc k => unfold $ rewrite PolyRing.zro_*c polyCoef_*

\lemma lastCoef_* {R : Ring} {p q : Poly R} : lastCoef (p * q) = lastCoef p * lastCoef q \elim p
  | pzero => inv zro_*-left
  | padd p e => polyCoef_+ *> zro-left *> polyCoef_*c

\lemma lastCoef_pow {R : Ring} {p : Poly R} {n : Nat} : lastCoef (pow p n) = R.pow (lastCoef p) n \elim n
  |  => idp
  | suc n => lastCoef_* *> pmap (`* _) lastCoef_pow

\func polyMapRingHom (f : RingHom) : RingHom (PolyRing f.Dom) (PolyRing f.Cod) \cowith
  | func => polyMap f
  | func-+ {p q : Poly f.Dom} : polyMap f (p + q) = polyMap f p + polyMap f q \elim p, q {
    | pzero, q => idp
    | padd p a, pzero => idp
    | padd p a, padd q b => rewrite (func-+,f.func-+) idp
  }
  | func-ide => rewrite func-ide idp
  | func-* {p q : Poly f.Dom} : polyMap f (p * q) = polyMap f p * polyMap f q \elim p {
    | pzero => idp
    | padd p e => func-+ *> pmap2 (+) (pmap2 padd func-* func-zro) polyMap_*c
  }
  \where
    \func polyMap_*c {f : RingHom} {a : f.Dom} {q : Poly f.Dom} : polyMap f (a PolyRing.*c q) = f a PolyRing.*c polyMap f q \elim q
      | pzero => idp
      | padd q b => pmap2 padd polyMap_*c f.func-*

\func polyEvalRingHom {R : CRing} (a : R) : RingHom (PolyRing R) R \cowith
  | func => polyEval __ a
  | func-+ {p q : Poly R} : polyEval (p + q) a = polyEval p a + polyEval q a \elim p, q {
    | pzero, q => inv zro-left
    | padd p x, pzero => inv zro-right
    | padd p x, padd q y => rewrite func-+ equation
  }
  | func-ide => equation
  | func-* {p q : Poly R} : polyEval (p * q) a = polyEval p a * polyEval q a \elim p {
    | pzero => inv zro_*-left
    | padd p x => func-+ *> rewrite (func-*,polyEval_*c) equation
  }
  \where
    \lemma polyEval_*c {R : Ring} {x a : R} {p : Poly R} : polyEval (x PolyRing.*c p) a = x * polyEval p a \elim p
      | pzero => inv zro_*-right
      | padd p y => rewrite polyEval_*c equation

\func polyMapEvalRingHom {R : Ring} {S : CRing} (f : RingHom R S) (a : S) : RingHom (PolyRing R) S
  => polyEvalRingHom a ∘ polyMapRingHom f
  \where
    \lemma polyMapEval_*c {R : Ring} {S : CRing} {f : RingHom R S} {x : R} {a : S} {p : Poly R} : polyMapEval f (x PolyRing.*c p) a = f x * polyMapEval f p a
      => pmap (polyEval __ a) polyMapRingHom.polyMap_*c *> polyEvalRingHom.polyEval_*c

\func polyMapEval-unique {R S : Ring} (f g : RingHom (PolyRing R) S) (p : \Pi (r : R) -> f (padd pzero r) = g (padd pzero r)) (q : f (padd  ) = g (padd  )) (x : PolyRing R) : f x = g x \elim x
  | pzero => f.func-zro *> inv g.func-zro
  | padd x e => pmap f padd-expand *> f.func-+ *> pmap2 (+) (f.func-* *> pmap2 (*) (polyMapEval-unique _ _ p q x) q *> inv g.func-*) (p e) *> inv g.func-+ *> inv (pmap g padd-expand)

\func degree {R : Ring.Dec} (p : Poly R) : Nat \elim p
  | pzero => 
  | padd p _ => \case decideEq p  \with {
    | yes _ => 
    | no _ => suc (degree p)
  }
  | peq => idp

\func degree< {R : AddPointed} (p : Poly R) (n : Nat)
  => \Pi {k : Nat} -> n <= k -> polyCoef p k = 

\lemma degree_degree< {R : Ring.Dec} {p : Poly R} {n : Nat} (d : degree p < n) : degree< p n \elim n
  | suc n => degree<=_degree< $ degree<=.fromDegree (<_suc_<= d)

\lemma degree<_degree {R : Ring.Dec} {p : Poly R} {n : Nat} (p/=0 : p /= ) (d : degree< p n) : degree p < n \elim n
  |  => absurd $ p/=0 $ degree<=.trivialPoly \lam k _ => d zero<=_
  | suc n => suc_<=_< $ suc<=suc $ degree<=.toDegree $ degree<_degree<= d

\lemma degree<_+ {R : Ring} {p q : Poly R} {n : Nat} (dp : degree< p n) (dq : degree< q n) : degree< (p + q) n
  => \lam s => polyCoef_+ *> pmap2 (+) (dp s) (dq s) *> zro-left

\lemma degree<_negative {R : Ring} {p : Poly R} {n : Nat} (dp : degree< p n) : degree< (negative p) n
  => \lam s => polyCoef_negative *> pmap negative (dp s) *> R.negative_zro

\lemma degree<0 {R : AddPointed} {p : Poly R} (d : degree< p ) : p = pzero
  => degree<=.trivialPoly (\lam k _ => d zero<=_)

\lemma degree<_padd {R : AddPointed} {p : Poly R} {e : R} {n : Nat} (d : degree< p n) : degree< (padd p e) (suc n)
  => \lam {k} => \case \elim k \with {
    |  => \lam s => absurd (s NatSemiring.zero<suc)
    | suc k => \lam s => d (suc<=suc.conv s)
  }
  \where
    \lemma conv {R : AddPointed} {p : Poly R} {e : R} {n : Nat} (d : degree< (padd p e) (suc n)) : degree< p n
      => \lam s => d (suc<=suc s)

\lemma degree<_polyMap {f : AddPointedHom} {p : Poly f.Dom} {n : Nat} (d : degree< p n) : degree< (polyMap f p) n \elim p, n
  | pzero, n => \lam _ => idp
  | padd p e,  =>
    \have t => padd=pzero (degree<0 d)
    \in rewrite (t., t., f.func-zro) $ transportInv (degree< __ ) peq \lam _ => idp
  | padd p e, suc n => degree<_padd $ degree<_polyMap (degree<_padd.conv d)

\lemma degree_polyMap {R S : Ring.Dec} {f : RingHom R S} (inj : isInj f) {p : Poly R} : degree (polyMap f p) = degree p \elim p
  | pzero => idp
  | padd p e => mcases {} \with {
    | yes p=0 => rewrite (decideEq=_reduce $ later $ rewrite p=0 idp) idp
    | no p/=0 => rewrite (decideEq/=_reduce \lam q => p/=0 $ polyMap-inj inj q) $ pmap suc (degree_polyMap inj)
  }

\lemma polyEval_polyCoef {R : Ring} {p : Poly R} {a : R} {n : Nat} (d : degree< p n) : polyEval p a = R.BigSum (\new Array R n (\lam i => polyCoef p i * R.pow a i)) \elim p, n
  | pzero, n => inv $ R.BigSum_zro \lam j => R.zro_*-left
  | p,  => rewrite (degree<0 d) idp
  | padd p e, suc n => rewrite (polyEval_polyCoef (degree<_padd.conv d)) $ pmap2 (+) (R.BigSum-rdistr *> pmap (\lam x => R.BigSum (\new Array R n x)) (ext \lam j => *-assoc)) (inv ide-right) *> +-comm

\lemma polyMapEval_polyCoef {f : RingHom} {p : Poly f.Dom} {a : f.Cod} {n : Nat} (d : degree< p n)
  : polyMapEval f p a = AddMonoid.BigSum (\lam (i : Fin n) => f (polyCoef p i) * pow a i)
  => polyEval_polyCoef (degree<_polyMap d) *> pmap AddMonoid.BigSum (exts \lam j => pmap (`* _) polyCoef_polyMap)

\func degree<= {R : AddPointed} (p : Poly R) (n : Nat) : \Prop
  | pzero, n => \Sigma
  | padd p a,  => p = pzero
  | padd p a, suc n => degree<= p n
  | peq,  => ext (\lam _ => (), \lam _ => idp)
  | peq, suc n => idp
  \where {
    \lemma toDegree {R : Ring.Dec} {p : Poly R} {n : Nat} (d : degree<= p n) : degree p <= n \elim p, n
      | pzero, n => zero<=_
      | padd p e,  => rewrite (decideEq=_reduce d) zero<=_
      | padd p e, suc n => mcases \with {
        | yes _ => zero<=_
        | no _ => suc<=suc (toDegree d)
      }

    \lemma fromDegree {R : Ring.Dec} {p : Poly R} {n : Nat} (q : degree p <= n) : degree<= p n \elim p, n
      | pzero, n => ()
      | padd p e,  => cases (decideEq p , q) \with {
        | yes r, q => r
        | no _, q => absurd (q NatSemiring.zero<suc)
      }
      | padd p e, suc n => fromDegree $ cases (decideEq p , q) \with {
        | yes r, q => rewrite r zero<=_
        | no n1, q => suc<=suc.conv q
      }

    \lemma toCoefs {R : AddPointed} (p : Poly R) (n : Nat) (d : degree<= p n) {k : Nat} (n<k : n < k) : polyCoef p k =  \elim p, n, k, n<k
      | pzero, n, k, _ => idp
      | padd p e, , suc k, _ => rewrite d idp
      | padd p e, suc n, suc k, NatSemiring.suc<suc n<k => toCoefs p n d n<k

    \lemma trivialPoly {R : AddPointed} {p : Poly R} (d : \Pi (k : Nat) -> degree<= p k -> polyCoef p k = ) : p = pzero
      => \case degree-exists p \with {
           | inP (n,dp) => aux d n dp
         }
      \where
        \lemma aux {R : AddPointed} {p : Poly R} (d : \Pi (k : Nat) -> degree<= p k -> polyCoef p k = ) (n : Nat) (dp : degree<= p n) : p = pzero \elim n
          |  => degree<=0 p dp *> pmap (padd pzero) (d  dp) *> peq
          | suc n => aux d n $ degree-reduce p n dp (d (suc n) dp)

    \lemma fromCoefs {R : AddPointed} (p : Poly R) (n : Nat) (d : \Pi {k : Nat} -> n < k -> polyCoef p k = ) : degree<= p n \elim p, n
      | pzero, n => ()
      | padd p e,  => trivialPoly (\lam k _ => d NatSemiring.zero<suc)
      | padd p e, suc n => fromCoefs p n (\lam n<k => d (NatSemiring.suc<suc n<k))
  }

\lemma degree<=_degree< {R : AddPointed} {p : Poly R} {n : Nat} (d : degree<= p n) : degree< p (suc n)
  => \lam s => degree<=.toCoefs p n d (id<suc <∘l s)

\lemma degree<_degree<= {R : AddPointed} {p : Poly R} {n : Nat} (d : degree< p (suc n)) : degree<= p n
  => degree<=.fromCoefs p n \lam q => d (suc_<_<= q)

\lemma degree<=_polyMap {f : AddPointedHom} {p : Poly f.Dom} {n : Nat} (d : degree<= p n) : degree<= (polyMap f p) n
  => degree<_degree<= $ degree<_polyMap (degree<=_degree< d)

\lemma degree-exists {R : AddPointed} (p : Poly R) : ∃ (n : Nat) (degree<= p n) \elim p
  | pzero => inP (, ())
  | padd p e => TruncP.map (degree-exists p) \lam s => (suc s., s.)

\lemma degree<-exists {R : AddPointed} (p : Poly R) : ∃ (n : Nat) (degree< p n)
  => TruncP.map (degree-exists p) \lam s => (suc s., degree<=_degree< s.)

\lemma degree<=-trans {R : AddPointed} {p : Poly R} {n m : Nat} (d : degree<= p n) (n<=m : n <= m) : degree<= p m \elim p, n, m
  | pzero, n, m => ()
  | padd p x, ,  => d
  | padd p x, suc n,  => absurd (n<=m NatSemiring.zero<suc)
  | padd p x, , suc m => rewrite d ()
  | padd p x, suc n, suc m => degree<=-trans d (suc<=suc.conv n<=m)

\lemma degree-reduce {R : AddPointed} (p : Poly R) (n : Nat) (d : degree<= p (suc n)) (c : polyCoef p (suc n) = ) : degree<= p n \elim p, n
  | pzero, n => ()
  | padd pzero e,  => idp
  | padd (padd p x) y,  => pmap2 padd d c *> peq
  | padd p e, suc n => degree-reduce p n d c

\lemma degree-monic-reduce {R : Ring} (p : Poly R) (a : R) (n : Nat) (d : degree<= (p * padd  a) (suc n)) : degree<= p n \elim p, n
  | pzero, n => ()
  | padd p e,  => \let t => degree<=0 _ $ transport (degree<= __ _) (+-assoc *> pmap (_ +) negative-right *> zro-right) $ degree<=_+ {_} {_} {negative (padd pzero (e * ))} d idp
                   \in (aux a _  (pmap (_ +) peq *> zro-right *> t)).
  | padd p e, suc n => degree-monic-reduce p a n $ transport (degree<= __ _) (+-assoc *> pmap (_ +) negative-right *> zro-right) $ degree<=_+ {_} {_} {negative (padd pzero (e * ))} d ()
  \where \private \lemma aux {p : Poly R} (a b c : R) (q : p * padd  a + padd pzero c = padd pzero b) : \Sigma (p = pzero) (c = b) \elim p
    | pzero => (idp, pmap (polyCoef __ ) q)
    | padd p e => \let t => aux _ _ _ $ inv zro-right *> pmap polyShift q *> inv peq
                  \in (pmap2 padd t. (inv ide-right *> t.) *> peq, inv zro-left *> pmap (`+ c) (inv $ zro-left *> pmap (`* _) (inv ide-right *> t.) *> R.zro_*-left) *> pmap (polyCoef __ ) q)

\lemma polyCoef-linear-* {R : Ring} (p q : Poly R) (a : R) (n : Nat) : polyCoef (padd q a * p) (suc n) = polyCoef (q * p) n + a * polyCoef p (suc n)
  => polyCoef_+ *> pmap (_ +) polyCoef_*c

\lemma degree<=0 {R : AddPointed} (p : Poly R) (d : degree<= p ) : p = padd pzero (polyCoef p ) \elim p
  | pzero => inv peq
  | padd p e => pmap (padd __ e) d

\lemma degree<=_+ {R : Ring} {p q : Poly R} {n : Nat} (dp : degree<= p n) (dq : degree<= q n) : degree<= (p + q) n \elim p, q, n
  | pzero, q, n => dq
  | padd p x, pzero, n => dp
  | padd p x, padd q y,  => pmap2 (+) dp dq
  | padd p x, padd q y, suc n => degree<=_+ dp dq

\lemma degree<=_BigSum {R : Ring} {l : Array (Poly R)} {n : Nat} (d : \Pi (j : Fin l.len) -> degree<= (l j) n) : degree<= (AddMonoid.BigSum l) n
  => AddMonoid.BigSum-pred {_} {degree<= __ n} () (\lam {p} {q} => degree<=_+) d

\lemma degree<=_FinSum {R : Ring} {J : FinSet} {a : J -> Poly R} {n : Nat} (d : \Pi (j : J) -> degree<= (a j) n) : degree<= (AbMonoid.FinSum a) n
  => AbMonoid.FinSum-pred {_} {degree<= __ n} () (\lam {p} {q} => degree<=_+) d

\lemma degree<=_*c {R : Ring} {a : R} {p : Poly R} {n : Nat} (d : degree<= p n) : degree<= (a PolyRing.*c p) n \elim p, n
  | pzero, n => ()
  | padd p e,  => pmap (a PolyRing.*c) d
  | padd p e, suc n => degree<=_*c d

\lemma degree<=_negative {R : Ring} {p : Poly R} {n : Nat} (d : degree<= p n) : degree<= (negative p) n \elim p, n
  | pzero, n => ()
  | padd p e,  => pmap negative d
  | padd p e, suc n => degree<=_negative d

\lemma degree<=_* {R : Ring} {p q : Poly R} {n m : Nat} (dp : degree<= p n) (dq : degree<= q m) : degree<= (p * q) (n + m) \elim p, n
  | pzero, n => ()
  | padd p e,  => rewrite dp $ transportInv (\lam x => degree<= (x + _) m) peq $ degree<=_*c dq
  | padd p e, suc n => degree<=_+ (later $ degree<=_* dp dq) (degree<=_*c $ degree<=-trans dq $ NatSemiring.<=_+ {} {suc n} zero<=_ <=-refl)

\lemma degree<=0_*-conv {R : StrictDomain} {p q : Poly R} (d : degree<= (p * q) ) : degree<= p  || degree<= q 
  => \case degree-exists p, degree-exists q \with {
    | inP dp, inP dq => aux dp. dq. d
  }
  \where {
    \lemma aux {R : StrictDomain} {p q : Poly R} {n m : Nat} (dp : degree<= p n) (dq : degree<= q m) (d : degree<= (p * q) )
      : degree<= p  || degree<= q  \elim n, m
      | , m => byLeft dp
      | suc n,  => byRight dq
      | suc n, suc m => \case zeroProduct $ inv (leadCoef-product dp dq) *> degree<=.toCoefs (p * q)  d {suc (suc (n + m))} NatSemiring.zero<suc \with {
        | byLeft c => aux (degree-reduce p n dp c) dq d
        | byRight c => aux dp (degree-reduce q m dq c) d
      }
  }

\lemma polyInv {R : StrictDomain} {p : Poly R} (pi : Inv p) : ∃ (r : R) (p = padd pzero r) (Inv r)
  => \have lem (dp : degree<= p ) (dq : degree<= pi.inv ) : ∃ (r : R) (p = padd pzero r) (Inv r)
           => inP (polyCoef p , degree<=0 p dp, \new Inv {
             | inv => lastCoef pi.inv
             | inv-left => inv zro-left *> pmap lastCoef (rewrite (degree<=0 p dp, degree<=0 pi.inv dq) in pi.inv-left)
             | inv-right => inv zro-left *> pmap lastCoef (rewrite (degree<=0 p dp, degree<=0 pi.inv dq) in pi.inv-right)
           })
     \in \case degree<=0_*-conv (rewrite pi.inv-right idp) \with {
       | byLeft d => lem d $ coefInv $ rewrite (degree<=0 p d, inv PolyRing.*c_*) in pi.inv-right
       | byRight d => lem (coefInv $ rewrite (degree<=0 pi.inv d, inv PolyRing.*c_*) in pi.inv-left) d
     }
  \where {
    \lemma coefInv {R : StrictDomain} {c : R} {p : Poly R} (q : c PolyRing.*c p = ) : degree<= p  \elim p
      | pzero => ()
      | padd p a => \case zeroProduct {_} {padd pzero c} (pmap (`+ _) peq *> zro-left *> pmap polyShift q) \with {
        | byLeft r => \have t => pmap lastCoef $ inv peq *> (rewrite (pmap (polyCoef __ ) r, zro_*-left, PolyRing.zro_*c) in q)
                      \in degree<=.trivialPoly \lam k _ => inv ide-right *> pmap (polyCoef p k *) (inv t) *> zro_*-right
        | byRight r => r
      }
  }

\lemma polyDiv {R : StrictDomain} {p q : Poly R} (p|q : LDiv p q) (q|p : LDiv q p)
  : (\Sigma (p = ) (q = )) || (\Sigma (a b : R) (p|q.inv = padd pzero a) (q|p.inv = padd pzero b) (a * b = ) (b * a = ))
  => \case StrictDomain.zeroOrCancel-left $ inv *-assoc *> pmap (`* _) p|q.inv-right *> q|p.inv-right *> inv ide-right \with {
    | byLeft p=0 => byLeft (p=0, inv p|q.inv-right *> pmap (`* _) p=0 *> zro_*-left {_} {p|q.inv})
    | byRight c => \case StrictDomain.zeroOrCancel-left $ inv *-assoc *> pmap (`* _) q|p.inv-right *> p|q.inv-right *> inv ide-right \with {
      | byLeft q=0 => byLeft (inv q|p.inv-right *> pmap (`* _) q=0 *> zro_*-left {_} {q|p.inv}, q=0)
      | byRight d => \case polyInv (\new Inv p|q.inv q|p.inv d c), polyInv (\new Inv q|p.inv p|q.inv c d) \with {
        | inP (a,u,a-inv), inP (b,v,b-inv) => byRight (a, b, u, v,
            inv zro-left *> pmap lastCoef (inv (pmap2 (*) u v) *> c),
            inv zro-left *> pmap lastCoef (inv (pmap2 (*) v u) *> d))
      }
    }
  }

\lemma polyDiv-linear {R : StrictIntegralDomain} {p q : Poly R} {l : Array R} (s : p * q = Monoid.BigProd (map (\lam a => padd  (negative a)) l))
  : (\Sigma (j : Fin l.len) (polyEval q (l j) = )) || Monoid.Inv q \elim l
  | nil => byRight (Monoid.Inv.lmake p s)
  | a :: l => \case R.zeroProduct {polyEval p a} {polyEval q a} (inv (func-* {polyEvalRingHom a}) *> pmap (polyEval __ a) s *> MonoidHom.func-BigProd {polyEvalRingHom a} {map (\lam a => padd  (negative a)) (a :: l)} *> pmap (`* _) (simplify simplify) *> zro_*-left) \with {
    | byLeft r => \have t => inv *-assoc *> pmap (`* _) *-comm *> (rewrite (rootDiv_* r) in s)
                  \in \case polyDiv-linear $ StrictDomain.nonZero-cancel-left {PolyStrictDomain R} {padd  (negative a)} (\lam c => R.zro/=ide $ inv $ pmap (polyCoef __ ) c) t \with {
                    | byLeft r => byLeft (suc r., r.)
                    | byRight r => byRight r
                  }
    | byRight r => byLeft (,r)
  }

\lemma monomial-factor {R : StrictIntegralDomain} {p q s : Poly R} (t : p * q = padd s )
  : ∃ (r : Poly R) (Or (\Sigma (p = padd r ) (r * q = s)) (\Sigma (q = padd r ) (p * r = s))) \elim p, q
  | pzero, q => inP (pzero, inl (inv peq, pmap polyShift t))
  | p, pzero => inP (pzero, inr (inv peq, zro_*-right *> pmap polyShift (inv zro_*-right *> t)))
  | padd p a, padd q b => \case zeroProduct $ inv zro-left *> pmap lastCoef t \with {
    | byLeft a=0 => inP (p, inl (pmap (padd p) a=0, *-comm *> inv zro-right *> pmap (_ +) (inv PolyRing.zro_*c *> pmap (`*c q) (inv a=0)) *> pmap (`+ _) *-comm *> pmap polyShift t))
    | byRight b=0 => inP (q, inr (pmap (padd q) b=0, pmap (`+ _) (inv zro-right *> pmap2 (\lam x => padd x  +) *-comm (inv PolyRing.zro_*c *> pmap (`*c p) (inv b=0)) *> *-comm) *> pmap polyShift t))
  }

\lemma monomial_div {R : StrictIntegralDomain} {n : Nat} {p : Poly R} (d : LDiv p (monomial  n)) : ∃ (c : R) (c /= ) (k : Nat) (p = monomial c k) \elim n, p
  | , p => TruncP.map (polyInv $ Inv.lmake d.inv $ *-comm *> d.inv-right) \lam s => (s., NonZeroSemiring.inv-nonZero s., , s.)
  | suc n, p => \case monomial-factor d.inv-right \with {
    | inP (r, inl s) => TruncP.map (monomial_div (\new LDiv r (monomial  n) d.inv s.)) \lam t => (t., t., suc t., s. *> pmap (padd __ ) t.)
    | inP (r, inr s) => monomial_div (\new LDiv p (monomial  n) r s.)
  }

\lemma monomial_div2 {R : Ring} {n : Nat} {c : R} {p : Poly R} (d : LDiv (monomial c (suc n)) p) : lastCoef p =  \elim p
  | pzero => idp
  | padd p a => pmap lastCoef $ inv $ pmap (_ +) (inv PolyRing.zro_*c) *> d.inv-right

\lemma degree<=_BigProd {R : Ring} {l : Array (Poly R)} (d : Array Nat l.len) (p : \Pi (j : Fin l.len) -> degree<= (l j) (d j))
  : degree<= (BigProd l) (AddMonoid.BigSum d) \elim l, d
  | nil, d => idp
  | a :: l, n :: d => degree<=_* (p ) $ degree<=_BigProd d \lam j => p (suc j)

\lemma degree<=_BigProd1 {R : Ring} {l : Array (Poly R)} (p : \Pi (j : Fin l.len) -> degree<= (l j) ) : degree<= (BigProd l) l.len
  => transport (degree<= _) Semiring.BigSum_replicate1 (degree<=_BigProd (replicate l.len ) p)

\lemma degree<=_pow {R : Ring} {p : Poly R} {d n : Nat} (pd : degree<= p d) : degree<= (pow p n) (d * n)
  => transport2 degree<= BigProd_replicate (Semiring.BigSum_replicate *> *-comm) (degree<=_BigProd {_} {replicate n p} (replicate n d) \lam _ => pd)

\lemma degree<=_monomial {R : AddPointed} {c : R} {n : Nat} : degree<= (monomial c n) n \elim n
  |  => idp
  | suc n => degree<=_monomial

\lemma fromArray_polyCoef {R : AddPointed} {n : Nat} {p : Poly R} (d : degree< p n) : p = Poly.fromArray (\new Array R n (\lam j => polyCoef p j)) \elim n, p
  | , p => degree<=.trivialPoly (\lam k _ => d zero<=_)
  | n, pzero => inv fromArray0
  | suc n, padd p e => pmap (padd __ e) $ fromArray_polyCoef \lam q => d (suc<=suc q)
  \where
    \lemma fromArray0 {n : Nat} : Poly.fromArray (replicate n R.zro) = pzero \elim n
      |  => idp
      | suc n => pmap (padd __ zro) fromArray0 *> peq

\lemma fromArray_degree< {R : AddPointed} {l : Array R} : degree< (Poly.fromArray l) l.len \elim l
  | nil => \lam _ => idp
  | a :: l => \lam {k} => \case \elim k \with {
    |  => \lam d => \case suc_<=_< d
    | suc k => \lam d => fromArray_degree< (suc<=suc.conv d)
  }

\lemma *c_monomial {R : Ring} {a c : R} {n : Nat} : a PolyRing.*c monomial c n = monomial (a * c) n \elim n
  |  => idp
  | suc n => pmap2 padd *c_monomial zro_*-right

\lemma leadCoef-product {R : Ring} {p q : Poly R} {n m : Nat} (dp : degree<= p n) (dq : degree<= q m) : polyCoef (p * q) (n + m) = polyCoef p n * polyCoef q m \elim p, n
  | pzero, n => inv zro_*-left
  | padd p x,  => polyCoef_+ *> pmap2 (+) (\case \elim m \with {
    |  => idp
    | suc m => later (rewrite dp idp)
  }) polyCoef_*c *> zro-left
  | padd p x, suc n => polyCoef_+ *> pmap2 (+) (leadCoef-product dp dq) (polyCoef_*c *> pmap (x *) (degree<=.toCoefs q m dq $ <_+-left m NatSemiring.zero<suc) *> zro_*-right) *> zro-right

\lemma leadCoef_BigProd {R : Ring} {l : Array (Poly R)} (d : Array Nat l.len) (ld : \Pi (j : Fin l.len) -> degree<= (l j) (d j))
  : polyCoef (BigProd l) (AddMonoid.BigSum d) = R.BigProd (\lam j => polyCoef (l j) (d j)) \elim l, d
  | nil, d => idp
  | p :: l, n :: d => leadCoef-product (ld ) (degree<=_BigProd d (\lam j => ld (suc j))) *> pmap (_ *) (leadCoef_BigProd d (\lam j => ld (suc j)))

\lemma leadCoef_BigProd1 {R : Ring} {l : Array (Poly R)} (ld : \Pi (j : Fin l.len) -> degree<= (l j) ) (lc : \Pi (j : Fin l.len) -> polyCoef (l j)  = ) : polyCoef (BigProd l) l.len = 
  => pmap (polyCoef _) (inv Semiring.BigSum_replicate1) *> leadCoef_BigProd (replicate l.len ) ld *> pmap BigProd (exts lc) *> BigProd_replicate1 {_} {l.len}

\lemma leadCoef_pow {R : Ring} {p : Poly R} {d n : Nat} (pd : degree<= p d) : polyCoef (pow p n) (d * n) = pow (polyCoef p d) n
  => pmap2 polyCoef (inv BigProd_replicate) (*-comm *> inv Semiring.BigSum_replicate) *> leadCoef_BigProd {R} {replicate n p} (replicate n d) (\lam _ => pd) *> BigProd_replicate

\func isMonic {R : Ring} (p : Poly R) : \Prop
  => ∃ (n : Nat) (degree<= p n) (polyCoef p n = )

\lemma polyMap_isMonic {f : RingHom} {p : Poly f.Dom} (m : isMonic p) : isMonic (polyMap f p) \elim m
  | inP t => inP (t., degree<=_polyMap t., polyCoef_polyMap *> pmap f t. *> func-ide)

\lemma field-toMonic {K : DiscreteField} {p : Poly K} (p/=0 : p /= ) : isMonic (finv (leadCoef p) *c p)
  => inP (degree p, degree<=_*c $ degree<=.fromDegree <=-refl, polyCoef_*c *> pmap (_ *) (inv leadCoef_polyCoef) *> K.finv-left \lam s => p/=0 (leadCoef=0-lem s))

\lemma monomial-isMonic {R : Ring} (n : Nat) : isMonic (monomial R.ide n)
  => inP (n, degree<=_monomial, polyCoef_monomial)

\lemma monic/=0 {R : Ring} {p : Poly R} (pm : isMonic p) (p=0 : p = ) :  = {R}  \elim pm
  | inP (n,d,q) => rewrite p=0 in q

\lemma monic-unique {R : Ring} {p : Poly R} {n m : Nat} (n/=m : n /= m) (d1 : degree<= p n) (c1 : polyCoef p n = ) (d2 : degree<= p m) (c2 : polyCoef p m = ) :  = {R} 
  => \case LinearOrder.trichotomy n m \with {
    | less n<m => inv (degree<=.toCoefs p n d1 n<m) *> c2
    | equals n=m => absurd (n/=m n=m)
    | greater m<n => inv (degree<=.toCoefs p m d2 m<n) *> c1
  }

\lemma monic-coef {R : Ring.Dec} {p : Poly R} (pm : isMonic p) : polyCoef p (degree p) =  \elim pm
  | inP (n,d,q) => \case LinearOrder.dec<_<= (degree p) n \with {
    | inl p<n => R.trivial (inv (degree_degree< p<n <=-refl) *> q)
    | inr n<=p => pmap (polyCoef p) (<=-antisymmetric (degree<=.toDegree d) n<=p) *> q
  }

\func polyDivision {R : CRing} (f g : Poly R) (k m n : Nat) (p : suc m = k + n) (df : degree<= f m) (dg : degree<= g n)
  : \Sigma (q r : Poly R) (pow (polyCoef g n) k *c f = q * g + r) (degree< r n) \elim k, m, n
  | , m, n => (pzero, f, PolyRing.ide_*c *> equation, rewriteI p $ degree<=_degree< df)
  | , ,  => (f, pzero, rewrite (degree<=0 g dg, ide-left, zro-right) $ PolyRing.*c_* *> *-comm, \lam _ => idp)
  | , , suc n => \case p
  | suc (suc k), , n => \case p
  | suc k, suc m, n => \let f1 => polyCoef g n *c f - monomial (polyCoef f (suc m)) k * g \in
                       \have rec => polyDivision f1 g k m n (pmap pred p) (degree-reduce f1 m
                                (degree<=_+ (degree<=_*c df) (degree<=_negative $ rewrite (pmap pred p) $ degree<=_* degree<=_monomial dg))
                                (polyCoef_+ *> pmap (_ +) polyCoef_negative *> rewrite polyCoef_*c (rewrite {} (pmap pred p) $ rewrite (polyCoef_*,*-comm) negative-right))) dg
                       \in (rec. + monomial (pow (polyCoef g n) k * polyCoef f (suc m)) k, rec., rewrite (PolyRing.*c-assoc, rdistr) $ unfold f1 (rewrite (PolyRing.*c-ldistr, PolyRing.*c_negative, PolyRing.*c-comm-left, *c_monomial) equation) *> pmap (_ +) rec. *> inv +-assoc *> pmap (`+ _) +-comm, rec.)

\lemma monicPolyDivisionContr {R : CRing} (f g : Poly R) (n : Nat) (dg : degree<= g n) (dm : polyCoef g n = ) : Contr (\Sigma (q r : Poly R) (f = q * g + r) (degree< r n))
  => \case degree-exists f \with {
       | inP (l,df) => isProp=>isContr (\lam s1 s2 =>
           \have | s : (s1. - s2.) * g = s2. - s1. => equation {CRing} {usingOnly {s1., s2.}}
                 | t => aux (s1. - s2.) g n dg dm $ rewrite s $ degree<_+ s2. $ degree<_negative s1.
           \in ext (AddGroup.fromZero t, inv $ AddGroup.fromZero $ inv s *> pmap (`* g) t))
           \have s => polyDivision f g (suc l) (l + n) n idp (degree<=-trans df $ NatSemiring.<=_+ <=-refl zero<=_) dg
           \in (s., s., later (rewrite dm $ inv $ pmap (`*c f) (R.pow_ide {suc l}) *> PolyRing.ide_*c) *> s., s.)
     }
  \where {
    \lemma aux {R : Ring} (q g : Poly R) (n : Nat) (dg : degree<= g n) (dm : polyCoef g n = ) (dqg : degree< (q * g) n) : q = 
      => degree<=.trivialPoly \lam k dq => inv (leadCoef-product dq dg *> pmap (_ *) dm *> ide-right) *> dqg (LinearlyOrderedSemiring.<=_+ zero<=_ <=-refl)
  }

\lemma monicPolyDivision-unique {R : CRing} (f g : Poly R) (n : Nat) (dg : degree<= g n) (dm : polyCoef g n = )
  : isProp (\Sigma (q r : Poly R) (f = q * g + r) (degree< r n))
  => isContr=>isProp (monicPolyDivisionContr f g n dg dm)

\lemma monicPolyDivision {R : CRing} (f g : Poly R) (n : Nat) (dg : degree<= g n) (dm : polyCoef g n = )
  : \Sigma (q r : Poly R) (f = q * g + r) (degree< r n) \level monicPolyDivision-unique f g n dg dm
  => Contr.center {monicPolyDivisionContr f g n dg dm}

\lemma degree1PolyDivision-unique {R : CRing} (f : Poly R) (a : R) {q1 q2 : Poly R} (p1 : f = q1 * padd  (negative a) + padd pzero (polyEval f a)) (p2 : f = q2 * padd  (negative a) + padd pzero (polyEval f a)) : q1 = q2
  => pmap __. $ monicPolyDivision-unique f (padd  (negative a))  idp idp  (q1, padd pzero (polyEval f a), p1, degree<=_degree< idp) (q2, padd pzero (polyEval f a), p2, degree<=_degree< idp)

\lemma degree1PolyDivision {R : CRing} (f : Poly R) (a : R)
  : \Sigma (q : Poly R) (f = q * padd  (negative a) + padd pzero (polyEval f a)) \level \lam s1 s2 => ext (degree1PolyDivision-unique f a s1. s2.)
  => \have t => monicPolyDivision f (padd  (negative a))  idp idp
     \in (t., t. *> pmap (_ +) (fromArray_polyCoef t. *> pmap (padd pzero) (later (repeat simplify (rewrite (fromArray_polyCoef t.) simplify)) *> inv (pmap (polyEval __ a) t. *> func-+ {polyEvalRingHom a} *> pmap (`+ _) func-*))))

\lemma rootPolyDivision-unique {R : CRing} (f : Poly R) (a : R) (p : polyEval f a = ) : isProp (LDiv (padd  (negative a)) f)
  => \lam s1 s2 => ext $ degree1PolyDivision-unique f a
       (inv (LDiv.inv-right {s1}) *> rewrite p (*-comm *> inv zro-right *> pmap (_ +) (inv peq)))
       (inv (LDiv.inv-right {s2}) *> rewrite p (*-comm *> inv zro-right *> pmap (_ +) (inv peq)))

\func rootDiv {R : CRing} (f : Poly R) (a : R) : Poly R
  => (degree1PolyDivision f a).

\lemma rootDiv_* {R : CRing} {f : Poly R} {a : R} (p : polyEval f a = )
  : f = rootDiv f a * padd  (negative a)
  => (degree1PolyDivision f a). *> pmap (_ +) (later $ rewrite p peq) *> zro-right

\lemma rootPolyDivision_degree {R : IntegralDomain.Dec} {f : Poly R} (f/=0 : f /= ) {a : R} (p : polyEval f a = ) {n : Nat} : degree f = suc (degree (rootDiv f a))
  => rewrite {} (rootDiv_* p *> *-comm) $ degree_* {_} {padd  (negative a)} (\lam p => R.zro/=ide $ inv $ pmap (polyCoef __ ) p) (\lam q => f/=0 $ rootDiv_* p *> *-comm *> cong q *> zro_*-right) *> rewrite (decideEq/=_reduce $ /=-sym zro/=ide) idp

\func leadCoef {R : Ring.Dec} (p : Poly R) : R \elim p
  | pzero => 
  | padd p e => \case decideEq p  \with {
    | yes _ => e
    | no _ => leadCoef p
  }
  | peq => idp

\lemma leadCoef_polyCoef {R : Ring.Dec} {p : Poly R} : leadCoef p = polyCoef p (degree p) \elim p
  | pzero => idp
  | padd p e => mcases \with {
    | yes p=0 => idp
    | no p/=0 => leadCoef_polyCoef
  }

\lemma leadCoef=0-lem {R : Ring.Dec} {p : Poly R} (s : leadCoef p = ) : p =  \elim p
  | pzero => idp
  | padd p a => cases (decideEq p , s) \with {
    | yes p=0, a=0 => pmap2 padd p=0 a=0 *> path peq
    | no p/=0, s => absurd $ p/=0 (leadCoef=0-lem s)
  }

\lemma leadCoef_monomial {R : Ring.Dec} {a : R} {n : Nat} : leadCoef (monomial a n) = a \elim n
  |  => idp
  | suc n => mcases \with {
    | yes e => inv (pmap leadCoef e) *> leadCoef_monomial
    | no _ => leadCoef_monomial
  }

\lemma degree_monomial {R : Ring.Dec} {a : R} {n : Nat} (a/=0 : a /= ) : degree (monomial a n) = n \elim n
  |  => idp
  | suc n => mcases \with {
    | yes e => absurd $ a/=0 $ inv leadCoef_monomial *> pmap leadCoef e
    | no _ => pmap suc (degree_monomial a/=0)
  }

\lemma degree=0-lem {R : Ring.Dec} {p : Poly R} (dp=0 : degree p = ) : p = padd pzero (leadCoef p) \elim p
  | pzero => inv peq
  | padd p a => mcases \with {
    | yes p=0 => pmap (padd __ a) p=0
    | no p/=0 => \case rewrite (decideEq/=_reduce p/=0) in dp=0
  }

\instance PolyDecCRing (R : CRing.Dec) : CRing.Dec
  | Ring.Dec => PolyDecRing R
  | *-comm => PolyAlgebra.*-comm

\instance PolyDecDomain (R : Domain.Dec) : Domain.Dec
  | Domain => PolyDomain R
  | decideEq => PolyDecRing.decideEq
  | nonZeroApart {p : Poly R} (p/=0 : p /= ) : #0 p \elim p {
    | pzero => p/=0 idp
    | padd p a => \case R.decideEq a  \with {
      | yes a=0 => byLeft $ nonZeroApart \lam p=0 => p/=0 $ pmap2 padd p=0 a=0 *> path peq
      | no n => byRight (R.nonZeroApart n)
    }
  }
  \where \open PolyRingWith#

\instance PolyDecIntegralDomain (R : IntegralDomain.Dec) : IntegralDomain.Dec
  | Domain.Dec => PolyDecDomain R
  | *-comm => PolyAlgebra.*-comm

\lemma degree_padd {R : Ring.Dec} {p : Poly R} (a : R) (p/=0 : p /= ) : degree (padd p a) = suc (degree p)
  => rewrite (decideEq/=_reduce p/=0) idp

\lemma degree_+ {R : Ring.Dec} {p q : Poly R} (q<p : degree q < degree p) : degree (p + q) = degree p \elim p, q
  | pzero, pzero => idp
  | pzero, padd q a => \case q<p
  | padd p a, pzero => idp
  | padd p a, padd q a' => cases (decideEq p , decideEq q , q<p) \with {
    | no p/=0, yes q=0, NatSemiring.zero<suc => rewrite (q=0, PolyRing.zro-right, decideEq/=_reduce p/=0) idp
    | no p/=0, no q/=0, NatSemiring.suc<suc q<p => mcases \with {
      | yes p+q=0 => \case rewrite (inv $ rewrite p+q=0 in degree_+ q<p) in q<p
      | no _ => pmap suc (degree_+ q<p)
    }
  }

\lemma leadCoef_+ {R : Ring.Dec} {p q : Poly R} (q<p : degree q < degree p) : leadCoef (p + q) = leadCoef p \elim p, q
  | pzero, pzero => idp
  | pzero, padd q a => \case q<p
  | padd p a, pzero => idp
  | padd p a, padd q a' => cases (decideEq p , decideEq q , q<p) \with {
    | no p/=0, yes q=0, NatSemiring.zero<suc => rewrite (q=0, PolyRing.zro-right, decideEq/=_reduce p/=0) idp
    | no p/=0, no q/=0, NatSemiring.suc<suc q<p => mcases \with {
      | yes p+q=0 => \case rewrite (inv $ rewrite p+q=0 in degree_+ q<p) in q<p
      | no _ => leadCoef_+ q<p
    }
  }

\lemma degree_*c {R : Domain.Dec} {c : R} {p : Poly R} (c/=0 : c /= ) : degree (c PolyRing.*c p) = degree p \elim p
  | pzero => idp
  | padd p a => mcases {} \with {
    | yes p=0 => rewrite p=0 idp
    | no p/=0 => rewrite (decideEq/=_reduce $ *c-nonZero c/=0 p/=0) $ pmap suc (degree_*c c/=0)
  }
  \where {
    \lemma *c-nonZero (c/=0 : c /= ) {p : Poly R} (p/=0 : p /= ) : c PolyRing.*c p /= 
      => transportInv (`/= ) PolyRing.*c_* $ Domain.nonZero_* {_} {padd pzero c} (\lam e => c/=0 $ pmap lastCoef e) p/=0
  }

\lemma degree_* {R : Domain.Dec} {p q : Poly R} (p/=0 : p /= ) (q/=0 : q /= ) : degree (p * q) = degree p + degree q \elim p
  | pzero => absurd (p/=0 idp)
  | padd p e => mcases \with {
    | yes p=0 => rewrite p=0 $ pmap (\lam x => degree (x + _)) peq *> degree_*c (\lam e=0 => p/=0 $ pmap2 padd p=0 e=0 *> path peq)
    | no p/=0' => degree_+ (later $ rewrite (decideEq/=_reduce $ Domain.nonZero_* p/=0' q/=0) (degree_< q/=0 p/=0')) *>
        rewrite (decideEq/=_reduce $ Domain.nonZero_* p/=0' q/=0) (pmap suc (degree_* p/=0' q/=0))
  }
  \where
    \lemma degree_< (q/=0 : q /= ) {a : R} {p : Poly R} (p/=0 : p /= ) : degree (a PolyRing.*c q) < suc (degree (p * q))
      => \case decideEq a  \with {
        | yes a=0 => rewrite (a=0,PolyRing.zro_*c) NatSemiring.zero<suc
        | no a/=0 => rewrite (degree_*c a/=0, degree_* p/=0 q/=0) $ LinearlyOrderedSemiring.<=_+ zero<=_ <=-refl <∘r id<suc
      }

\lemma degree_*_= {R : Domain.Dec} {p q s : Poly R} (s/=0 : s /= ) (t : s = p * q) : degree s = degree p + degree q
  => pmap degree t *> degree_* (\lam p=0 => s/=0 $ t *> pmap (`* q) p=0) (\lam q=0 => s/=0 $ t *> pmap (p *) q=0 *> zro_*-right)

\lemma leadCoef_*c {R : Domain.Dec} {a : R} {p : Poly R} : leadCoef (a PolyRing.*c p) = a * leadCoef p \elim p
  | pzero => inv R.zro_*-right
  | padd p e => mcases {} \with {
    | yes p=0 => rewrite p=0 idp
    | no p/=0 => \case decideEq a  \with {
      | yes a=0 => rewrite (a=0,PolyRing.zro_*c) simplify
      | no a/=0 => rewrite (decideEq/=_reduce $ degree_*c.*c-nonZero a/=0 p/=0) leadCoef_*c
    }
  }

\lemma leadCoef_* {R : Domain.Dec} {p q : Poly R} : leadCoef (p * q) = leadCoef p * leadCoef q \elim p
  | pzero => inv R.zro_*-left
  | padd p e => mcases \with {
    | yes p=0 => rewrite p=0 $ pmap (leadCoef $ __ + _) peq *> leadCoef_*c
    | no p/=0 => \case decideEq q  \with {
      | yes q=0 => rewrite (q=0, Ring.zro_*-right {PolyRing R}) (inv R.zro_*-right)
      | no q/=0 => leadCoef_+ (later $ rewrite (decideEq/=_reduce $ Domain.nonZero_* p/=0 q/=0) (degree_*.degree_< q/=0 p/=0)) *> rewrite (decideEq/=_reduce $ Domain.nonZero_* p/=0 q/=0) leadCoef_*
    }
  }

\func poly-factor-monomial {R : AddPointed} {D : DecSet R} {p : Poly R}
  : p /= pzero -> \Sigma (n : Nat) (q : Poly R) (p = iterr (padd __ ) n q) (lastCoef q /= ) \elim p
  | pzero => \lam p/=0 => absurd (p/=0 idp)
  | padd p a => \lam pX+a/=0 => \case decideEq a  \with {
    | yes a=0 => \have s => poly-factor-monomial \lam p=0 => pX+a/=0 $ pmap2 padd p=0 a=0 *> peq
                 \in (suc s., s., rewrite a=0 $ pmap (padd __ ) s., s.)
    | no a/=0 => (, padd p a, idp, a/=0)
  }
  | peq => pathOver $ simp_coe \lam f => absurd (f idp)

\lemma poly-factor-monomial-unique {R : AddPointed} {n m : Nat} {q q' : Poly R} (c : iterr (padd __ ) n q = iterr (padd __ ) m q') (qc : lastCoef q /= ) (q'c : lastCoef q' /= ) : \Sigma (n = m) (q = q') \elim n, m
  | ,  => (idp, c)
  | , suc m => absurd $ qc $ rewrite c idp
  | suc n,  => absurd $ q'c $ rewriteI c idp
  | suc n, suc m => \have r => poly-factor-monomial-unique (pmap polyShift c) qc q'c
                    \in (pmap suc r., r.)

\lemma poly-monomial-char {R : Ring} {n : Nat} {p : Poly R} : monomial  n * p = iterr (padd __ ) n p \elim n
  |  => pmap2 (+) peq PolyRing.ide_*c
  | suc n => pmap (_ +) PolyRing.zro_*c *> pmap (padd __ ) poly-monomial-char

\instance PolyEuclideanRingData (R : DiscreteField) : EuclideanRingData (Poly R)
  | CRing => PolyAlgebra R
  | decideEq => PolyDecRing.decideEq
  | euclideanMap => degree
  | divMod p q => \case decideEq (degree q)  \with {
    | yes _ => \case decideEq q  \with {
      | yes _ => (,p)
      | no _ => (finv (leadCoef q) PolyRing.*c p, )
    }
    | no _ => divMod_fuel p q (EuclideanSemiringData.suc' (degree p))
  }
  | isDivMod p q => cases (decideEq (degree q) ) \with {
    | yes dq=0 => mcases \with {
      | yes _ => pmap (`+ p) Ring.zro_*-right
      | no q/=0 => zro-right *> pmap (`* _) (degree=0-lem dq=0) *> pmap (`+ _) peq *> inv PolyRing.*c-assoc *> pmap (PolyRing.`*c p) (R.finv-right (q/=0 $ leadCoef=0-lem __)) *> PolyRing.ide_*c
    }
    | no dq/=0 => divMod_fuel-correct p q dq/=0 $ rewrite EuclideanSemiringData.suc'=suc id<suc
  }
  | isEuclideanMap p q q/=0 => cases (decideEq (degree q) ) \with {
    | yes dq=0 => rewrite (decideEq/=_reduce q/=0) \lam r/=0 => absurd (r/=0 idp)
    | no dq/=0 => \lam _ => divMod_fuel-rem-lem p q dq/=0
  }
  \where {
    \func divMod_fuel {R : DiscreteField} (p q : Poly R) (n : Nat) : \Sigma (Poly R) (Poly R) \elim n
      |  => (,)
      | suc n => \case LinearOrder.dec<_<= (degree p) (degree q) \with {
        | inl _ => (,p)
        | inr _ =>
          \let | m => monomial (leadCoef p * finv (leadCoef q)) (degree p -' degree q)
               | (d,r) => divMod_fuel (p - m * q) q n
          \in (d + m, r)
      }

    \lemma divMod_fuel-correct {R : DiscreteField} (p q : Poly R) (dq/=0 : degree q /= ) {n : Nat} (s : degree p < n) : q * (divMod_fuel p q n). + (divMod_fuel p q n). = p \elim n
      |  => \case s
      | suc n => mcases \with {
        | inl p<q => pmap (`+ p) Ring.zro_*-right
        | inr q<=p =>
          \let | p/=0 : p /=  => dq/=0 $ <=_exists $ rewrite __ in q<=p
               | q/=0 => dq/=0 $ pmap degree __
               | lq/=0 => q/=0 $ leadCoef=0-lem __
               | m => monomial (leadCoef p * finv (leadCoef q)) (degree p -' degree q)
               | lm/=0 : leadCoef p * finv (leadCoef q) /=  => Domain.nonZero_* (p/=0 $ leadCoef=0-lem __) (R.inv-nonZero $ R.finv-Inv lq/=0)
               | dp=dmq : degree p = degree (m * q) => inv $ degree_* (transportInv (`/= ) (leadCoef_monomial {R}) lm/=0 $ pmap leadCoef __) q/=0 *> rewrite (degree_monomial lm/=0) (+-comm *> <=_exists q<=p)
          \in equation {CRing} {usingOnly (divMod_fuel-correct (p - m * q) q dq/=0 $ diff-lem dp=dmq (inv $ leadCoef_* *> pmap (`* _) leadCoef_monomial *> *-assoc *> pmap (_ *) (R.finv-left lq/=0) *> ide-right) (\lam dmq=0 => dq/=0 $ <=_exists $ transport (_ <=) (dp=dmq *> dmq=0) q<=p) <∘l <_suc_<= s)}
      }

    \lemma divMod_fuel-rem-lem {R : DiscreteField} (p q : Poly R) (dq/=0 : degree q /= ) {n : Nat} : degree (divMod_fuel p q n). < degree q \elim n
      |  => nonZero>0 dq/=0
      | suc n => mcases \with {
        | inl p<q => p<q
        | inr q<=p => divMod_fuel-rem-lem _ q dq/=0
      }

    \lemma diff-lem {R : Ring.Dec} {p q : Poly R} (s : degree p = degree q) (t : leadCoef p = leadCoef q) (dq/=0 : degree q /= ) : degree (p - q) < degree p \elim p, q
      | _, pzero => absurd (dq/=0 idp)
      | pzero, padd q a => absurd (cases (decideEq q , s, t) \with {
        | yes q=0, _, a=0 => dq/=0 $ rewrite (decideEq=_reduce q=0) idp
      })
      | padd p a, padd q a' => cases (decideEq p , decideEq q , s, t) \with {
        | yes p=0, yes q=0, _, a=a' => absurd $ (rewrite (decideEq=_reduce q=0) in dq/=0) idp
        | no p/=0, no q/=0, s, t => mcases \with {
          | yes _ => NatSemiring.zero<suc
          | no p-q/=0 => NatSemiring.suc<suc $ diff-lem (pmap pred s) t
              \lam dq=0 => p-q/=0 $ AddGroup.toZero $ degree=0-lem (pmap pred s *> dq=0) *> pmap (padd pzero) t *> inv (degree=0-lem dq=0)
        }
      }
  }

\instance PolyEuclideanDomain (R : DiscreteField) : EuclideanDomain (Poly R)
  | IntegralDomain.Dec => PolyDecIntegralDomain R
  | isEuclidean => inP (PolyEuclideanRingData R)

\lemma poly-dec-unit {R : DiscreteField} (p : Poly R) : Dec (Inv p) \elim p
  | pzero => no \lam e => NonZeroSemiring.inv-nonZero e idp
  | padd p a => \case decideEq p , decideEq a  \with {
    | yes p=0, no a/=0 => yes $ rewrite p=0 $ Inv.lmake (padd pzero (finv a)) $ pmap (padd pzero) $ zro-left *> R.finv-left a/=0
    | yes p=0, yes a=0 => no \lam e => NonZeroSemiring.inv-nonZero e $ pmap2 padd p=0 a=0 *> peq
    | no p/=0, _ => no \lam e => \case polyInv e \with {
      | inP (_,q,_) => p/=0 (pmap polyShift q)
    }
  }

\lemma poly-dec-div {R : DiscreteField} (a b : Poly R) : Dec (TruncP (LDiv a b))
  => GCDDomain.Dec.div_unit. poly-dec-unit a b

\func poly-maximal-ideal {K : DiscreteField} (c : Countable K) (p : Poly K) (pc : Not (Inv p))
  : \Sigma (M : Ideal (PolyAlgebra K)) M.IsMaximal (M p)
  => \let (M,Mm,g) => BezoutRing.maximal-ideal (Poly.poly-countable c) poly-dec-div (p :: nil) (\lam c => pc $ c p \lam () => LDiv.id-div)
     \in (M, Mm, g )

\func polyModule {R : Ring} {U : LModule R} (f : LinearMap U U) : LModule (PolyRing R) \cowith
  | AbGroup => U
  | *c p u => poly_func p f u
  | *c-assoc {p q : Poly R} {a : U} : poly_func (p * q) f a = poly_func p f (poly_func q f a) \elim p {
    | pzero => idp
    | padd p e => *c-rdistr *> rewrite (U.*c_zro-left,zro-right) (pmap2 (+) (pmap f *c-assoc) poly_func_poly-*c)
  }
  | *c-ldistr {p : Poly R} {a b : U} : poly_func p f (a + b) = poly_func p f a + poly_func p f b \elim p {
    | pzero => inv zro-left
    | padd p e => pmap (f __ + _) *c-ldistr *> pmap2 (+) f.func-+ U.*c-ldistr *> equation
  }
  | *c-rdistr {p q : Poly R} {a : U} : poly_func (p + q) f a = poly_func p f a + poly_func q f a \elim p, q {
    | pzero, q => inv zro-left
    | padd p b, pzero => inv zro-right
    | padd p b, padd q c => pmap (f __ + _) *c-rdistr *> pmap2 (+) f.func-+ U.*c-rdistr *> equation
  }
  | ide_*c => pmap2 (+) f.func-zro ide_*c *> zro-left
  \where {
    \func poly_func {R : Ring} {U : LModule R} (p : Poly R) (f : AddPointedHom U U) (u : U) : U \elim p
      | pzero => 
      | padd p e => f (poly_func p f u) + e *c u
      | peq => pmap2 (+) f.func-zro U.*c_zro-left *> zro-left

    \lemma poly_func_zro {R : Ring} {U : LModule R} {p : Poly R} {f : AddPointedHom U U} : poly_func p f  =  \elim p
      | pzero => idp
      | padd p e => pmap2 (f __ + __) poly_func_zro U.*c_zro-right *> zro-right *> f.func-zro

    \lemma poly_func_poly-*c {R : Ring} {U : LModule R} {a : R} {p : Poly R} {f : LinearMap U U} {u : U} : poly_func (a PolyRing.*c p) f u = a *c poly_func p f u \elim p
      | pzero => inv U.*c_zro-right
      | padd p e => pmap2 (+) (pmap f poly_func_poly-*c *> f.func-*c) U.*c-assoc *> inv U.*c-ldistr

    \lemma finitelyGenerated {R : Ring} {U : LModule R} {f : LinearMap U U} (fg : U.IsFinitelyGenerated) : LModule.IsFinitelyGenerated {polyModule f} \elim fg
      | inP (l,lg) => inP (l, \lam x => TruncP.map (lg x) \lam s => (map (padd pzero) s., s. *> pmap U.BigSum (exts \lam j => inv $ pmap (`+ _) f.func-zro *> zro-left)))
  }