\import Algebra.Meta
\import Algebra.Pointed
\import Arith.Nat
\import Data.Array
\import Data.Array.EPerm
\import Data.Array.Perm
\import Data.Fin (fsuc, fsuc/=, nat_fin_=)
\import Data.Or
\import Equiv
\import Equiv.Sigma
\import Equiv.Univalence.Set
\import Function
\import Function.Meta
\import Logic.Unique
\import Logic
\import Logic.Meta
\import Meta
\import Order.Biordered
\import Order.LinearOrder
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin
\import Set.Fin.BoundedPigeonhole
\import Set.Fin.Instances
\import Set.Fin.Pigeonhole

\class Semigroup \extends BaseSet {
  | \infixl  * : E -> E -> E
  | *-assoc {x y z : E} : (x * y) * z = x * (y * z)

  \func IsSquare (x : E) => ∃ (y : E) (y * y = x)

  \protected \func op : Semigroup E \cowith
    | * x y => y * x
    | *-assoc => inv *-assoc
}

\class Monoid \extends Pointed, Semigroup {
  | ide-left {x : E} : ide * x = x
  | ide-right {x : E} : x * ide = x

  \func pow (a : E) (n : Nat) : E \elim n
    |  => ide
    | suc n => pow a n * a

  \lemma pow_+ {a : E} {n m : Nat} : pow a (n + m) = pow a n * pow a m \elim m
    |  => inv ide-right
    | suc m => pmap (* a) pow_+ *> *-assoc

  \lemma pow_* {a : E} {n m : Nat} : pow a (n Nat.* m) = pow (pow a n) m \elim m
    |  => idp
    | suc m => pow_+ *> pmap (* _) pow_*

  \lemma pow-comm1 {a b : E} (p : a * b = b * a) {n : Nat} : pow a n * b = b * pow a n \elim n
    |  => ide-left *> inv ide-right
    | suc n => equation.monoid {p, pow-comm1 p}

  \lemma pow-comm2 {a b : E} (p : a * b = b * a) {n m : Nat} : pow a n * pow b m = pow b m * pow a n
    => pow-comm1 $ inv $ pow-comm1 (inv p)

  \lemma pow-comm {a b : E} (p : a * b = b * a) {n : Nat} : pow (a * b) n = pow a n * pow b n \elim n
    |  => inv ide-left
    | suc n => equation.monoid {pow-comm p, pow-comm1 (inv p)}

  \lemma pow_ide {n : Nat} : pow ide n = ide \elim n
    |  => idp
    | suc n => ide-right *> pow_ide

  \lemma pow-left {a : E} {n : Nat} : a * pow a n = pow a n * a
    => inv (pow-comm1 idp)

  \func BigProd (l : Array E) => Big (*) ide l

  \lemma BigProd-ext {n : Nat} {l l' : Array E n} (p : \Pi (i : Fin n) -> l i = l' i) : BigProd l = BigProd l'
    => pmap BigProd (arrayExt p)

  \lemma BigProd_ide {l : Array E} (p : \Pi (j : Fin l.len) -> l j = ide) : BigProd l = ide
    => AddMonoid.BigSum_zro {AddMonoid.fromMonoid \this} p

  \lemma BigProd-unique {l : Array E} (i : Fin l.len) (p : \Pi (j : Fin l.len) -> i /= j -> l j = ) : BigProd l = l i
    => AddMonoid.BigSum-unique {AddMonoid.fromMonoid \this} i p

  \lemma BigProd_++ {l l' : Array E} : BigProd (l ++ l') = BigProd l * BigProd l'
    => AddMonoid.BigSum_++ {AddMonoid.fromMonoid \this}

  \lemma BigProd_suc {n : Nat} {l : Array E (suc n)} : BigProd l = BigProd (\new Array E n (\lam i => l i)) * l (n Nat.mod suc n)
    => AddMonoid.BigSum_suc {AddMonoid.fromMonoid \this}

  \lemma BigProd_replicate {x : E} {n : Nat} : BigProd (replicate n x) = pow x n \elim n
    |  => idp
    | suc n => pmap (x *) BigProd_replicate *> pow-left

  \lemma BigProd_replicate1 {n : Nat} : BigProd (replicate n ide) = ide
    => BigProd_replicate *> pow_ide

  \func IsCentral (x : E) : \Prop
    => \Pi (y : E) -> x * y = y * x

  \lemma IsCentral_ide : IsCentral 
    => \lam y => ide-left *> inv ide-right

  \lemma IsCentral_* {x y : E} (xc : IsCentral x) (yc : IsCentral y) : IsCentral (x * y)
    => \lam z => *-assoc *> pmap (x *) (yc z) *> inv *-assoc *> pmap (* y) (xc z) *> *-assoc

  \lemma IsCentral_pow {x : E} (xc : IsCentral x) {n : Nat} : IsCentral (pow x n) \elim n
    |  => IsCentral_ide
    | suc n => IsCentral_* (IsCentral_pow xc) xc

  \protected \func op : Monoid E \cowith
    | ide => ide
    | * x y => y * x
    | ide-left => ide-right
    | ide-right => ide-left
    | *-assoc => inv *-assoc
} \where {
  \protected \func equals.{u} {M N : Monoid.{u}} (p : M = {\Set u} N) (q : \let f x => coe (p @) x right \in \Pi (x y : M) -> f (x * y) = f x * f y) : M = {Monoid.{u}} N
    => exts (p, ide-equality, q)
    \where {
      \lemma ide-equality : coe (p @) ide right = ide
        => \let | f x => coe (p @) x right
                | g y => coe (inv p @) y right
                | fg y : f (g y) = y => transport_id_inv (\lam Z => Z) p y
           \in f ide             ==< inv ide-left >==
               ide * f ide       ==< pmap (* f ide) (inv (fg ide)) >==
               f (g ide) * f ide ==< inv (q (g ide) ide) >==
               f (g ide * ide)   ==< pmap f ide-right >==
               f (g ide)         ==< fg ide >==
               ide               `qed
    }

  \record DivBase {M : Monoid} (\coerce val : M) (elem inv : M)

  -- | The type of left divisors of an element
  \record LDiv \extends DivBase
    | inv-right : val * inv = elem
    \where {
      \func make {M : Monoid} {a b : M} (c : M) (p : a * c = b) : LDiv a b
        => \new LDiv { | inv => c | inv-right => p }

      \lemma product {M : CMonoid} {x y z w : M} (x|y : LDiv x y) (z|w : LDiv z w) : LDiv (x * z) (y * w) (z|w.inv * x|y.inv) \cowith
        | inv-right => *-assoc *> pmap (x *) (inv *-assoc *> pmap (* _) z|w.inv-right *> *-comm) *> inv *-assoc *> pmap (* w) x|y.inv-right

      \lemma product-left {M : Monoid} (x : M) {y z : M} (y|z : LDiv y z) : LDiv (x * y) (x * z) y|z.inv \cowith
        | inv-right =>
            (x * y) * y|z.inv ==< *-assoc >==
            x * (y * y|z.inv) ==< pmap (x *) y|z.inv-right >==
            x * z             `qed

      \lemma product-right {M : CMonoid} (z : M) {x y : M} (x|y : LDiv x y) : LDiv (x * z) (y * z) x|y.inv \cowith
        | inv-right =>
            (x * z) * x|y.inv ==< pmap (* x|y.inv) *-comm >==
            (z * x) * x|y.inv ==< *-assoc >==
            z * (x * x|y.inv) ==< pmap (z *) x|y.inv-right >==
            z * y             ==< *-comm >==
            y * z             `qed

      \lemma factor-left {M : Monoid} {x y z : M} (x|y : LDiv x y) : LDiv x (y * z) (x|y.inv * z) \cowith
        | inv-right => inv *-assoc *> pmap (* z) x|y.inv-right

      \lemma factor-right {M : CMonoid} {x y z : M} (x|z : LDiv x z) : LDiv x (y * z) (x|z.inv * y) \cowith
        | inv-right => inv *-assoc *> pmap (* y) x|z.inv-right *> *-comm

      \lemma cancel-left {M : CancelMonoid} (x : M) {y z : M} (x*y|x*z : LDiv (x * y) (x * z)) : LDiv y z x*y|x*z.inv \cowith
        | inv-right => M.cancel_*-left x (
            x * (y * x*y|x*z.inv) ==< inv *-assoc >==
            (x * y) * x*y|x*z.inv ==< x*y|x*z.inv-right >==
            x * z                 `qed)

      \lemma cancel-right {M : CancelCMonoid} {x y : M} (z : M) (x*z|y*z : LDiv (x * z) (y * z)) : LDiv x y x*z|y*z.inv \cowith
        | inv-right => M.cancel_*-right z (
            (x * x*z|y*z.inv) * z ==< *-comm >==
            z * (x * x*z|y*z.inv) ==< inv *-assoc >==
            (z * x) * x*z|y*z.inv ==< pmap (* x*z|y*z.inv) *-comm >==
            (x * z) * x*z|y*z.inv ==< x*z|y*z.inv-right >==
            y * z                 `qed)

      \lemma trans {M : Monoid} {x y z : M} (x|y : LDiv x y) (y|z : LDiv y z) : LDiv x z (x|y.inv * y|z.inv) \cowith
        | inv-right =>
            x * (x|y.inv * y|z.inv) ==< inv *-assoc >==
            (x * x|y.inv) * y|z.inv ==< pmap (* y|z.inv) x|y.inv-right >==
            y * y|z.inv             ==< y|z.inv-right >==
            z                       `qed

      \lemma ide-div {M : Monoid} {x : M} : LDiv ide x x \cowith
        | inv-right => ide-left

      \lemma id-div {M : Monoid} {x : M} : LDiv x x ide \cowith
        | inv-right => ide-right

      \lemma swap {M : CMonoid} (l : LDiv {M}) : LDiv l.inv l.elem l.val \cowith
        | inv-right => *-comm *> l.inv-right

      \lemma idempt {M : Monoid} (l : LDiv {M}) (p : l * l = l) : l * l.elem = l.elem
        => inv (*-assoc *> pmap (l *) l.inv-right) *> pmap (* _) p *> l.inv-right

      \use \lemma cancelProp {M : Monoid} (x : M) (q : \Pi {a b : M} -> x * a = x * b -> a = b) (y : M) : isProp (LDiv x y) =>
        \lam (d1 d2 : LDiv x y) =>
            \have p => q (d1.inv-right *> inv d2.inv-right)
            \in path (\lam i => \new LDiv x y (p @ i) (prop-dpi (x * (p @ __) = y) d1.inv-right d2.inv-right @ i))

      \lemma fromTruncP {M : Monoid} {x y : M} (q : \Pi {a b : M} -> x * a = x * b -> a = b) (t : TruncP (LDiv x y))
        : LDiv x y \level cancelProp x q y \elim t
        | inP x|y => x|y

      \use \level levelProp {M : CancelMonoid} (x y : M) : isProp (LDiv x y) => cancelProp x (M.cancel_*-left x) y
    }

  -- | The type of right divisors of an element
  \record RDiv \extends DivBase
    | inv-left : inv * val = elem
    \where {
      \lemma product-right {M : Monoid} (x y z : M) (x|y : RDiv x y) : RDiv (x * z) (y * z) x|y.inv \cowith
        | inv-left =>
            x|y.inv * (x * z) ==< inv *-assoc >==
            (x|y.inv * x) * z ==< pmap (* z) x|y.inv-left >==
            y * z             `qed

      \lemma cancel-right {M : CancelMonoid} (x y z : M) (x*z|y*z : RDiv (x * z) (y * z)) : RDiv x y x*z|y*z.inv \cowith
        | inv-left => M.cancel_*-right z (
            (x*z|y*z.inv * x) * z ==< *-assoc >==
            x*z|y*z.inv * (x * z) ==< x*z|y*z.inv-left >==
            y * z                 `qed)

      \lemma trans {M : Monoid} (x y z : M) (x|y : RDiv x y) (y|z : RDiv y z) : RDiv x z (y|z.inv * x|y.inv) \cowith
        | inv-left =>
            (y|z.inv * x|y.inv) * x ==< *-assoc >==
            y|z.inv * (x|y.inv * x) ==< pmap (y|z.inv *) x|y.inv-left >==
            y|z.inv * y             ==< y|z.inv-left >==
            z                       `qed

      \lemma levelProp {M : CancelMonoid} (x y : M) : isProp (RDiv x y) =>
        \lam (d1 d2 : RDiv x y) =>
            \have p => M.cancel_*-right x (d1.inv-left *> inv d2.inv-left)
            \in path (\lam i => \new RDiv x y (p @ i) (prop-dpi ((p @ __) * x = y) d1.inv-left d2.inv-left @ i))
    }

  -- | The type of left inverses of an element
  \record LInv \extends RDiv {
    | elem => ide

    \lemma inv-cancel-left {y z : M} (p : val * y = val * z) : y = z
      => inv ide-left *> pmap (* _) (inv inv-left) *> *-assoc *> pmap (_ *) p *> inv *-assoc *> pmap (* _) inv-left *> ide-left

    \lemma rotate-inv-left {x y : M} (p : val * x = y) : x = RInv.inv * y
      => inv ide-left *> pmap (* x) (inv inv-left) *> *-assoc *> pmap (_ *) p

    \lemma rotate-right {x y : M} (p : x * LInv.inv = y) : x = y * val
      => inv ide-right *> pmap (x *) (inv inv-left) *> inv *-assoc *> pmap (* _) p
  }

  -- | The type of right inverses of an element
  \record RInv \extends LDiv {
    | elem => ide

    \lemma inv-cancel-right {x y : M} (p : x * val = y * val) : x = y
      => inv ide-right *> pmap (_ *) (inv inv-right) *> inv *-assoc *> pmap (* _) p *> *-assoc *> pmap (_ *) inv-right *> ide-right

    \lemma rotate-inv-right {x y : M} (p : x * val = y) : x = y * RInv.inv
      => inv ide-right *> pmap (x *) (inv inv-right) *> inv *-assoc *> pmap (* _) p

    \lemma rotate-left {x y : M} (p : LInv.inv * x = y) : x = val * y
      => inv ide-left *> pmap (* x) (inv inv-right) *> *-assoc *> pmap (_ *) p
  }

  -- | The type of two-sided inverses of an element
  \record Inv \extends LInv, RInv {
    \protected \func reverse : Inv DivBase.inv val \cowith
      | inv-left => inv-right
      | inv-right => inv-left
  } \where {
      \use \lemma inv-isUnique {M : Monoid} (j j' : Inv {M}) (p : j.val = j'.val) : j.inv = j'.inv =>
        j.inv                 ==< inv ide-left >==
        ide * j.inv           ==< pmap (* j.inv) (inv j'.inv-left) >==
        (j'.inv * j') * j.inv ==< pmap ((_ * __) * _) (inv p) >==
        (j'.inv * j) * j.inv  ==< *-assoc >==
        j'.inv * (j * j.inv)  ==< pmap (j'.inv *) j.inv-right >==
        j'.inv * ide          ==< ide-right >==
        j'.inv                `qed

      \use \level levelProp {M : Monoid} {x : M} (j j' : Inv x) : j = j' =>
        \have p => inv-isUnique j j' idp
        \in path (\lam i => \new Inv x (p @ i)
                                     (prop-dpi ((p @ __) * x = ide) j.inv-left j'.inv-left @ i)
                                     (prop-dpi (x * (p @ __) = ide) j.inv-right j'.inv-right @ i))

      \lemma ide-isInv {M : Monoid} : Inv {M} ide \cowith
        | inv => ide
        | inv-left => ide-left
        | inv-right => ide-left

      \lemma product {M : Monoid} (i j : Inv {M}) : Inv (i * j) => func
        \where {
          \func func : Inv (i * j) \cowith
            | inv => j.inv * i.inv
            | inv-left => lem i j
            | inv-right => lem (\new Inv j.inv j.val j.inv-right j.inv-left) (\new Inv i.inv i.val i.inv-right i.inv-left)

          \lemma lem {M : Monoid} (i j : Inv {M}) : (j.inv * i.inv) * (i * j) = ide =>
            (j.inv * i.inv) * (i * j) ==< *-assoc >==
            j.inv * (i.inv * (i * j)) ==< pmap (j.inv *) (inv *-assoc) >==
            j.inv * ((i.inv * i) * j) ==< pmap (j.inv * (__ * j)) i.inv-left >==
            j.inv * (ide * j)         ==< pmap (j.inv *) ide-left >==
            j.inv * j                 ==< j.inv-left >==
            ide                       `qed
        }

    \lemma Inv_* {M : Monoid} {x y : M} (xi : Inv x) (yi : Inv y) : Inv (x * y)
      => product xi yi

    \lemma Inv_pow {M : Monoid} {x : M} (xi : Inv x) {n : Nat} : Inv (M.pow x n) \elim n
      |  => ide-isInv
      | suc n => Inv_* (Inv_pow xi) xi

    \lemma prod {M : Monoid} (i j : Inv {M}) : Inv (i * j) (j.inv * i.inv) => product.func

      \lemma factor-right {M : Monoid} {x y : M} (i : LInv x) (j : Inv (x * y)) : Inv y \cowith
        | inv => j.inv * x
        | inv-left => *-assoc *> j.inv-left
        | inv-right =>
          y * (j.inv * x)                 ==< inv ide-left >==
          ide * (y * (j.inv * x))         ==< pmap (* (y * (j.inv * x))) (inv i.inv-left) >==
          (i.inv * x) * (y * (j.inv * x)) ==< *-assoc >==
          i.inv * (x * (y * (j.inv * x))) ==< pmap (i.inv *) (inv *-assoc) >==
          i.inv * ((x * y) * (j.inv * x)) ==< pmap (i.inv *) (inv *-assoc) >==
          i.inv * (((x * y) * j.inv) * x) ==< pmap (i.inv * (__ * x)) j.inv-right >==
          i.inv * (ide * x)               ==< pmap (i.inv *) ide-left >==
          i.inv * x                       ==< i.inv-left >==
          ide                             `qed

      \lemma factor-left {M : Monoid} {x y : M} (i : RInv y) (j : Inv (x * y)) : Inv x =>
        \have t : Inv {M.op} x => factor-right {M.op} (\new LInv y i.inv i.inv-right) (\new Inv (x * y) j.inv j.inv-right j.inv-left)
        \in \new Inv t.val t.inv t.inv-right t.inv-left

      \lemma lmake {M : CMonoid} {x : M} (y : M) (p : y * x = ide) : Inv x y \cowith
        | inv-left => p
        | inv-right => *-comm *> p

      \lemma rmake {M : CMonoid} {x : M} (y : M) (p : x * y = ide) : Inv x y \cowith
        | inv-left => *-comm *> p
        | inv-right => p

      \lemma ldiv {M : CMonoid} {x : M} (d : LDiv x ide) : Inv x d.inv \cowith
        | inv-left => *-comm *> d.inv-right
        | inv-right => d.inv-right

      \lemma rdiv {M : CMonoid} {x : M} (d : RDiv x ide) : Inv x d.inv \cowith
        | inv-left => d.inv-left
        | inv-right => *-comm *> d.inv-left

      \lemma cfactor-right {M : CMonoid} {x y : M} (i : Inv (x * y)) : Inv y
        => lmake (i.inv * x) (*-assoc *> i.inv-left)

      \lemma cfactor-left {M : CMonoid} {x y : M} (i : Inv (x * y)) : Inv x
        => cfactor-right (transport (Inv __) *-comm i)

      \lemma Inv_LDiv {M : CMonoid} {x : M} (xi : Inv x) {y : M} (y|x : LDiv y x) : Inv y
        => cfactor-left $ transportInv Inv y|x.inv-right xi
    }
}

\func associates {M : Monoid} (x y : M) => \Sigma (u : Monoid.Inv {M}) (x = u * y)
  \where {
    \use \level levelProp {M : CancelMonoid} (x y : M) (t t' : associates x y) : t = t'
      => \have eq => cancel_*-right y (inv t. *> t'.)
         \in ext (ext (eq, Monoid.Inv.inv-isUnique t. t'. eq))
  }

\func associates-sym {M : Monoid} {x y : M} (a : associates x y) : associates y x
  => (Monoid.Inv.reverse {a.}, inv $ pmap (_ *) a. *> inv *-assoc *> pmap (* y) a..inv-left *> ide-left)

\class AddMonoid \extends AddPointed {
  | \infixl  + : E -> E -> E
  | zro-left {x : E} : zro + x = x
  | zro-right {x : E} : x + zro = x
  | +-assoc {x y z : E} : (x + y) + z = x + (y + z)

  \lemma negative-unique {x z : E} (y : E) (p : x + y = zro) (q : y + z = zro) : x = z
    => inv (+-assoc *> pmap (x +) q *> zro-right) *> pmap (+ z) p *> zro-left

  \func \infixl  *n (n : Nat) (a : E) : E \elim n
    |  => zro
    | suc n => n *n a + a

  \protected \lemma *n_pow {n : Nat} {a : E} : n *n a = \this.pow a n \elim n
    |  => idp
    | suc n => pmap (+ a) *n_pow

  \lemma *n-rdistr {n m : Nat} {a : E} : (n Nat.+ m) *n a = n *n a + m *n a
    => *n_pow *> \this.pow_+ *> inv (pmap2 (+) *n_pow *n_pow)

  \lemma *n-assoc {n m : Nat} {a : E} : (n Nat.* m) *n a = n *n (m *n a)
    => pmap (*n a) NatSemiring.*-comm *> *n_pow *> \this.pow_* *> inv *n_pow *> pmap (n *n) (inv *n_pow)

  \func BigSum (l : Array E) => Big (+) zro l

  \lemma BigSum-ext {n : Nat} {l l' : Array E n} (p : \Pi (i : Fin n) -> l i = l' i) : BigSum l = BigSum l'
    => pmap BigSum (arrayExt p)

  \lemma BigSum_++ {l l' : Array E} : BigSum (l ++ l') = BigSum l + BigSum l' \elim l
    | nil => inv zro-left
    | :: a l => unfold BigSum (rewrite BigSum_++ (inv +-assoc))

  \lemma BigSum_Big++ {ls : Array (Array E)} : BigSum (Big (++) nil ls) = BigSum (map BigSum ls) \elim ls
    | nil => idp
    | l :: ls => BigSum_++ *> pmap (_ +) BigSum_Big++

  \lemma BigSum_++' {l : Array E} {n : Nat} {l' : Array E n} : BigSum (l ++' l') = BigSum l + BigSum l' \elim l
    | nil => inv zro-left
    | a :: l => pmap (a +) BigSum_++' *> inv +-assoc

  \lemma BigSum-split {n m : Nat} {l : Array E (n Nat.+ m)}
    : BigSum l = BigSum (\lam (i : Fin n) => l (fin-inc i)) + BigSum (\lam (j : Fin m) => l (fin-raise j)) \elim n, l
    | , l => inv zro-left
    | suc n, a :: l => pmap (a +) BigSum-split *> inv +-assoc

  \lemma BigSum_suc {n : Nat} {l : Array E (suc n)} : BigSum l = BigSum (\new Array E n (\lam i => l i)) + l (n Nat.mod suc n) \elim n, l
    | , :: a nil => simplify
    | suc n, :: a l => pmap (a +) (BigSum_suc {_} {n} {l} *> pmap (_ + (a :: l) __) (fin_nat-inj (pmap suc (mod_< id<suc) *> inv (mod_< id<suc)))) *> inv +-assoc

  \lemma BigSum_suc-nat {n : Nat} {f : Nat -> E} : BigSum (\new Array E (suc n) (f __)) = BigSum (\new Array E n (f __)) + f n
    => BigSum_suc {_} {n} {f __} *> pmap (_ + f __) (mod_< id<suc)

  \lemma BigSum_zro {l : Array E} (p : \Pi (j : Fin l.len) -> l j = zro) : BigSum l = zro \elim l
    | nil => idp
    | :: a arr => pmap2 (+) (p ) (BigSum_zro (\lam j => p (suc j))) *> zro-left

  \lemma BigSum-unique {l : Array E} (i : Fin l.len) (p : \Pi (j : Fin l.len) -> i /= j -> l j = ) : BigSum l = l i \elim l, i
    | a :: l,  => pmap (a +) (BigSum_zro \lam j => p (suc j) (\case __)) *> zro-right
    | a :: l, suc i => pmap (a +) (BigSum-unique i \lam j q => p (suc j) (fsuc/= q)) *> pmap (+ l i) (p  (\case __)) *> zro-left

  \lemma BigSum-unique2 {l : Array E} {i j : Fin l.len} (i<j : i NatOrder.< j) (p : \Pi (k : Fin l.len) -> k /= i -> k /= j -> l k = ) : BigSum l = l i + l j \elim l, i, j, i<j
    | a :: l, , suc j, _ => pmap (a +) $ BigSum-unique j \lam k j/=k => p (suc k) (\case __) $ fsuc/= \lam q => j/=k (inv q)
    | a :: l, suc i, suc j, NatOrder.suc<suc i<j => pmap (+ _) (p  (\case __) (\case __)) *> zro-left *> BigSum-unique2 i<j (\lam k k/=i k/=j => p (suc k) (fsuc/= k/=i) (fsuc/= k/=j))

  \lemma BigSum-pred {P : E -> \Prop} (P0 : P ) (P+ : \Pi {x y : E} -> P x -> P y -> P (x + y)) {l : Array E} (p : \Pi (j : Fin l.len) -> P (l j)) : P (BigSum l) \elim l
    | nil => P0
    | a :: l => P+ (p ) $ BigSum-pred P0 P+ \lam j => p (suc j)

  \lemma BigSum_replicate0 {n : Nat} : BigSum (replicate n zro) =  \elim n
    |  => idp
    | suc n => zro-left *> BigSum_replicate0

  \lemma BigSum-subset {l l' : Array E} (p : l.len <= l'.len) (q1 : \Pi (j : Fin l.len) -> l j = l' (toFin j $ fin_< j <∘l p)) (q2 : \Pi (j : Fin l'.len) -> l.len <= j -> l' j = ) : BigSum l = BigSum l' \elim l, l'
    | nil, l => inv $ BigSum_zro \lam j => q2 j zero<=_
    | a :: l, nil => absurd linarith
    | a :: l, a' :: l' => pmap2 (+) (q1 ) $ BigSum-subset (suc<=suc.conv p) (\lam j => q1 (suc j)) (\lam j p => q2 (suc j) (suc<=suc p))

  \lemma fit_BigSum {n : Nat} {l : Array E} (p : \Pi (j : Fin l.len) -> n <= j -> l j = ) : BigSum (fit  {n} l) = BigSum l \elim n, l
    | , l => inv $ BigSum_zro \lam j => p j zero<=_
    | suc n, nil => BigSum_replicate0 {_} {suc n}
    | suc n, a :: l => pmap (a +) $ fit_BigSum \lam j n<=j => p (suc j) (suc<=suc n<=j)

  \lemma fit-transpose {n m : Nat} (l : Array (Array E m) n) : BigSum (\lam j => fit zro (l j) j) = BigSum (\lam k => fit zro (l __ k) k) \elim n, m, l
    | , , nil => idp
    | , suc m, nil => inv $ BigSum_replicate0 {_} {suc m}
    | suc n, , c :: l => BigSum_replicate0 {_} {suc n}
    | suc n, suc m, c :: l => pmap (c  +) $ fit-transpose \lam i => \lam j => l i (suc j)

  \protected \func op : AddMonoid E \cowith
    | zro => 
    | + a b => b + a
    | zro-left => zro-right
    | zro-right => zro-left
    | +-assoc => inv +-assoc
} \where {
    \use \coerce fromMonoid (M : Monoid) => \new AddMonoid M.E M.ide (M.*) M.ide-left M.ide-right M.*-assoc
    \use \coerce toMonoid (M : AddMonoid) => \new Monoid M.E M.zro (M.+) M.+-assoc M.zro-left M.zro-right
  }

\class CSemigroup \extends Semigroup
  | *-comm {x y : E} : x * y = y * x

\class CMonoid \extends Monoid, CSemigroup {
  \default ide-left => *-comm *> ide-right
  \default ide-right => *-comm *> ide-left

  \lemma divInv {x y : E} (cancel : \Pi {a b : E} -> x * a = x * b -> a = b) (xy|x : LDiv (x * y) x) : Inv y
    => Inv.lmake xy|x.inv (*-comm *> cancel (inv *-assoc *> xy|x.inv-right *> inv ide-right))

  \lemma pow_*-comm {a b : E} {n : Nat} : pow (a * b) n = pow a n * pow b n
    => pow-comm *-comm

  \func DivChain : \Prop
    => \Pi (a : Nat -> E) -> (\Pi (i : Nat) -> TruncP (LDiv (a (suc i)) (a i))) -> ∃ (j : Nat) (LDiv (a j) (a (suc j)))

  \lemma BigProd_* {n : Nat} {l l' : Array E n} : BigProd (\lam i => l i * l' i) = BigProd l * BigProd l'
    => AbMonoid.BigSum_+ {AbMonoid.fromCMonoid \this}

  \lemma BigProd_pow {k : Nat} {l : Array E} : BigProd (\lam i => pow (l i) k) = pow (BigProd l) k \elim k
    |  => BigProd_replicate1
    | suc k => BigProd_* {_} {_} {\lam i => pow (l i) k} *> pmap (* _) BigProd_pow

  \lemma BigProd_EPerm {l l' : Array E} (e : EPerm l l') : BigProd l = BigProd l'
    => AbMonoid.BigSum_EPerm {AbMonoid.fromCMonoid \this} e

  \lemma BigProd_Perm {n : Nat} {l l' : Array E n} (p : Perm l l') : BigProd l = BigProd l'
    => AbMonoid.BigSum_Perm {AbMonoid.fromCMonoid \this} p

  \func LDiv_BigProd {l : Array E} (j : Fin l.len) : LDiv (l j) (BigProd l) \elim l, j
    | a :: l,  => LDiv.factor-left LDiv.id-div
    | a :: l, suc j => LDiv.trans (LDiv_BigProd j) (LDiv.factor-right LDiv.id-div)

  \func LDiv_BigProd-coord {n : Nat} {l l' : Array E n} (p : \Pi (j : Fin n) -> LDiv (l j) (l' j)) : LDiv (BigProd l) (BigProd l') \elim n, l, l'
    | , nil, nil => LDiv.ide-div
    | suc n, a :: l, a' :: l' => LDiv.product (p ) $ LDiv_BigProd-coord \lam j => p (suc j)

  \lemma LDiv_BigProd_TruncP {n : Nat} {l l' : Array E n} (p : \Pi (j : Fin n) -> TruncP (LDiv (l j) (l' j))) : TruncP (LDiv (BigProd l) (BigProd l'))
    => TruncP.map (FinSet.finiteAC p) LDiv_BigProd-coord

  \func IsRegularElem (a : E) => \Pi {x y : E} -> a * x = a * y -> x = y

  \lemma LDiv_IsRegular {a b : E} (d : LDiv a b) (c : IsRegularElem b) : IsRegularElem a
    => \lam p => c $ pmap (* _) (inv d.inv-right *> *-comm) *> *-assoc *> pmap (d.inv *) p *> inv *-assoc *> pmap (* _) (*-comm *> d.inv-right)
} \where \open Monoid

\class AbMonoid \extends AddMonoid {
  | +-comm {x y : E} : x + y = y + x
  \default zro-left => +-comm *> zro-right
  \default zro-right => +-comm *> zro-left

  \lemma *n-ldistr {n : Nat} {a b : E} : n *n (a + b) = n *n a + n *n b \elim n
    |  => inv zro-left
    | suc n => inv +-assoc *> pmap (+ b) (pmap (+ a) *n-ldistr *> +-assoc *> pmap (_ +) +-comm *> inv +-assoc) *> +-assoc

  \lemma BigSum_+ {n : Nat} {l l' : Array E n} : BigSum (\lam i => l i + l' i) = BigSum l + BigSum l' \elim n, l, l'
    | , _, _ => inv zro-left
    | suc n, :: a l, :: a' l' => unfold BigSum $ rewrite (BigSum_+ {_} {n} {l}) equation.abMonoid

  \lemma BigSum-transpose {m n : Nat} (f : Fin m -> Fin n -> E)
    : BigSum (\lam i => BigSum (f i)) = BigSum (\lam j => BigSum (f __ j)) \elim n
    |  => BigSum_zro (\lam _ => idp)
    | suc _ => BigSum_+ *> pmap (_ +) (BigSum-transpose _)

  \lemma BigSum-double-dep {n : Nat} (m : Fin n -> Nat) (y : (\Sigma (i : Fin n) (Fin (m i))) -> E)
    : BigSum (\lam i => BigSum (\lam j => y (i,j))) = BigSum (\lam k => y (SigmaFin.aux.f k)) \elim n
    |  => idp
    | suc n => pmap (_ +) (BigSum-double-dep (\lam i => m (suc i)) (\lam p => y (suc p., p.))) *> inv (FinSum_Or *> pmap2 (+) FinSum=BigSum FinSum=BigSum) *> FinSum_Equiv OrFin.aux {\lam k => y (\case k \with {| inl s => (,s) | inr t => (suc (SigmaFin.aux.f t)., (SigmaFin.aux.f t).) })} *> FinSum=BigSum

  \lemma BigSum_Or {n m : Nat} (x : Or (Fin n) (Fin m) -> E)
    : BigSum (\lam j => x (OrFin.aux j)) = BigSum (\lam j => x (inl j)) + BigSum (\lam j => x (inr j)) \elim n
    |  => inv zro-left
    | suc n => pmap (_ +) (BigSum_Or (\lam a => x (Or.map a fsuc id))) *> inv +-assoc

  \lemma BigSum_EPerm {l l' : Array E} (e : EPerm l l') : BigSum l = BigSum l' \elim l, l', e
    | nil, nil, eperm-nil => idp
    | x :: l1, y :: l2, eperm-:: p e => pmap2 (+) p (BigSum_EPerm e)
    | x :: (x' :: l1), y :: (y' :: l2), eperm-swap idp idp r => equation.abMonoid {pmap BigSum r}
    | l, l', eperm-trans e1 e2 => BigSum_EPerm e1 *> BigSum_EPerm e2

  \lemma BigSum_Perm {n : Nat} {l l' : Array E n} (p : Perm l l') : BigSum l = BigSum l'
    => BigSum_EPerm (EPerm.Perm_EPerm p)

  -- | Reversing an array preserves its BigSum.
  \lemma BigSum-reverse {k : Nat} (l : Array E (suc k))
    : BigSum (\new Array E (suc k) (\lam i => l ((k -' i) Nat.mod suc k))) = BigSum l
    => BigSum_Perm {_} {suc k} reverse-perm
    \where {
      -- | The permutation that reverses an array of length `suc k`.
      \private \func reverse-perm {A : \Set} {k : Nat} {l : Array A (suc k)}
        : Perm (mkArray (\lam i => l ((k -' i) Nat.mod suc k))) l
        => Perm.perm-map {Fin (suc k)} {A} l {suc k} {\lam j => (k -' j) Nat.mod suc k} {\lam j => j}
          (Perm.perm-fin {suc k} (\lam j => (k -' j) Nat.mod suc k)
            (\lam {a} {a'} p => run {
              \have a<=k : a <= k => <_suc_<= (fin_< a),
              \have a'<=k : a' <= k => <_suc_<= (fin_< a'),
              nat_fin_= (rewrite (mod_< $ suc_<=_< (suc<=suc -'<=id), mod_< $ suc_<=_< (suc<=suc -'<=id), -'_inv a<=k, -'_inv a'<=k) in pmap (k -' __) p)
            }))
    }

  \sfunc FinSum {A : FinSet} (x : A -> E) : E
    => aux.
    \where {
      \lemma aux : \Sigma (r : E) (∃ (e : QEquiv {Fin A.card} {A}) (BigSum (\lam j => x (e j)) = r))
        => TruncP.rec-set A.finEq _ aux
        \where
          \lemma aux (e e' : QEquiv {Fin A.card} {A}) : BigSum (\lam j => x (e j)) = BigSum (\lam j => x (e' j))
            => BigSum_Perm $ transport (Perm _) (arrayExt \lam j => pmap x $ e.f_ret _) $ Perm.equiv_perm $ transQEquiv e' (symQEquiv e)
    }

  \lemma FinSum_char {A : FinSet} (x : A -> E) : ∃ (e : QEquiv {Fin A.card} {A}) (FinSum {_} {A} x = BigSum (\lam j => x (e j)))
    => TruncP.map FinSum.aux. \lam t => (t., (\peval FinSum {_} {A} x) *> inv t.)

  \lemma FinSum_char2 {A : FinSet} {x : A -> E} (e : QEquiv {Fin A.card} {A}) : FinSum x = BigSum (\lam j => x (e j))
    => \case FinSum_char x \with {
      | inP p => p. *> FinSum.aux.aux {_} {_} {x} p. e
    }

  \lemma FinSum_zro {J : FinSet} {x : J -> E} (p : \Pi (j : J) -> x j = ) : FinSum x = 
    => \case FinSum_char x \with {
      | inP (e,q) => q *> BigSum_zro (\lam j => p (e j))
    }

  \lemma FinSum_+ {J : FinSet} {x : J -> E} {y : J -> E} : FinSum (\lam j => x j + y j) = FinSum x + FinSum y
    => \case FinSum_char x \with {
      | inP (e,xp) => FinSum_char2 e *> BigSum_+ *> inv (pmap2 (+) xp (FinSum_char2 e))
    }

  \lemma FinSum-const {A : FinSet} {x : E} : FinSum {_} {A} (\lam _ => x) = BigSum (\new Array E A.card (\lam j => x))
    => \case FinSum_char {_} {A} (\lam _ => x) \with {
         | inP p => p.
       }

  \lemma FinSum-double-dep {A : FinSet} (B : A -> FinSet) {x : (\Sigma (a : A) (B a)) -> E}
    : FinSum (\lam a => FinSum (\lam b => x (a,b))) = FinSum {_} {SigmaFin A B} x
    => \case FinSum_char _, FinSet.choice (\lam a => FinSum_char (\lam b => x (a,b))) \with {
      | inP p, inP f => p. *> cong (ext \lam j => (f _).) *> BigSum-double-dep (\lam j => (B (p. j)).card) (\lam s => x (p. s., (f _). s.)) *>
                          inv (FinSum_char2 (unfold $ =-to-QEquiv (pmap Fin $ FinSum_char2 {NatSemiring} p.) `transQEquiv` SigmaFin.aux `transQEquiv` sigma-equiv p. (\lam j => (f _).)) *> pmap BigSum (exts $ (FinSum_char2 {NatSemiring} p., \lam j => idp)))
    }

  \lemma FinSum-double-dep' {A : FinSet} (B : A -> FinSet) {x : \Pi (a : A) -> B a -> E}
    : FinSum (\lam a => FinSum (x a)) = FinSum {_} {SigmaFin A B} \lam s => x s. s.
    => FinSum-double-dep B

  \lemma FinSum-double {A B : FinSet} {x : A -> B -> E}
    : FinSum (\lam a => FinSum (\lam b => x a b)) = FinSum (\lam (p : \Sigma A B) => x p. p.)
    => FinSum-double-dep (\lam _ => B) *> pmap {FinSet (\Sigma A B)} (FinSum {_} {__} _) prop-pi

  \lemma FinSum=BigSum {n : Nat} {x : Fin n -> E} : FinSum x = BigSum x
    => FinSum_char2 idEquiv

  \lemma FinSum-ext {A : FinSet} {x y : A -> E} (p : \Pi (a : A) -> x a = y a) : FinSum x = FinSum y
    => pmap FinSum (ext p)

  \lemma FinSum_Equiv {A B : FinSet} (e : QEquiv {A} {B}) {x : B -> E} : FinSum x = FinSum (\lam a => x (e a))
    => \case FinSum_char _ \with {
      | inP p => \let A' => \new FinSet A B.card { | finEq => TruncP.map B.finEq \lam e' => transQEquiv e' (symQEquiv e)}
                 \in FinSum_char2 (transQEquiv p. e) *> inv p. *> pmap {FinSet A} (FinSum {_} {__} _) (FinSet.levelProp A' A)
    }

  \lemma FinSum_Equiv2 {A B : FinSet} (e : QEquiv {A} {B}) {x : A -> E} {y : B -> E} (p : \Pi (a : A) -> x a = y (e a)) : FinSum x = FinSum y
    => pmap FinSum (ext p) *> inv (FinSum_Equiv e)

  \lemma FinSum-inj {A B : FinSet} (f : A -> B) (inj : IsInj f) {x : B -> E} (p : \Pi (b : B) -> (\Pi (a : A) -> f a /= b) -> x b = ) : FinSum x = FinSum (\lam a => x (f a))
    => FinSum_Equiv (later equiv)
    *> FinSum_Or {_} {SigmaFin B \lam b => DecFin (decide {dec b})} {SigmaFin B \lam b => DecFin (decide {NotDecide (dec b)})}
    *> pmap2 (+) (FinSum_Equiv $ later $ equiv2 inj) (FinSum_zro $ later \lam j => p j. \lam a q => j. $ inP (a,q)) *> zro-right
    \where {
      \protected \lemma dec (b : B) : Decide (∃ (a : A) (f a = b))
        => \new Decide { | decide => FinSet.search (\lam a => f a = b) (\lam a => decideEq (f a) b) }

      \protected \func equiv : QEquiv {Or (Given (b : B) ∃ (a : A) (f a = b)) (Given (b : B) (Not (∃ (a : A) (f a = b))))} {B} \cowith
        | f => \case __ \with {
          | inl s => s.
          | inr s => s.
        }
        | ret b => \case decide {dec b} \with {
          | yes e => inl (b,e)
          | no q => inr (b,q)
        }
        | ret_f => \case \elim __ \with {
          | inl s => rewrite (dec_yes_reduce s.) idp
          | inr s => rewrite (dec_no_reduce s.) idp
        }
        | f_sec b => mcases {} idp

      \protected \func equiv2 {A B : FinSet} {f : A -> B} (inj : IsInj f)
        => QEquiv.fromInjSurj {A} {\Sigma (b : B) (∃ (a : A) (f a = b))} {\lam a => (f a, inP (a,idp))}
            (\lam {a} {a'} q => inj $ pmap __. q)
            (\lam s => TruncP.map s. \lam t => (t., ext t.))
    }

  \lemma FinSum-inj2 {A B : FinSet} (f : A -> B) (inj : IsInj f) {x : B -> E} (p : \Pi (b : B) -> (\Pi (a : A) -> f a /= b) -> x b = )
                     {y : A -> E} (q : \Pi (a : A) -> x (f a) = y a) : FinSum x = FinSum y
    => FinSum-inj f inj p *> FinSum-ext q

  \lemma FinSum_Or {A B : FinSet} {x : Or A B -> E} : FinSum x = FinSum (\lam a => x (inl a)) + FinSum (\lam b => x (inr b))
    => \case FinSum_char _, FinSum_char _ \with {
      | inP p, inP q => FinSum_char2 (transQEquiv (OrFin.aux {A.card} {B.card}) (Or.Or_QEquiv p. q.)) *> BigSum_Or (\lam a => x (Or.map a p. q.)) *> inv (pmap2 (+) p. q.)
    }

  \lemma FinSum-unique {J : FinSet} {a : J -> E} (j : J) (p : \Pi (j' : J) -> j' /= j -> a j' = ) : FinSum a = a j
    => \case FinSum_char a \with {
         | inP (e,q) => q *> BigSum-unique (e.ret j) (\lam i c => p (e i) \lam s => c $ inv $ e.adjoint s) *> pmap a (e.f_ret j)
       }

  \lemma FinSum-unique2 {J : FinSet} {i j : J} (i/=j : i /= j) {x : J -> E} (p : \Pi (k : J) -> k /= i -> k /= j -> x k = ) : FinSum x = x i + x j
    => \case FinSum_char x \with {
      | inP (e,q) => q *> \case LinearOrder.dec<_<= {NatSemiring} (e.ret i) (e.ret j) \with {
        | inl i<j => BigSum-unique2 i<j (\lam k k/=i k/=j => p (e k) (\lam ek=i => k/=i $ inv (e.ret_f k) *> pmap e.ret ek=i) (\lam ek=j => k/=j $ inv (e.ret_f k) *> pmap e.ret ek=j)) *> pmap2 (x __ + x __) (e.f_ret i) (e.f_ret j)
        | inr j<=i => BigSum-unique2 (\case LinearOrder.dec<_<= {NatSemiring} (e.ret j) (e.ret i) \with {
          | inl j<i => j<i
          | inr i<=j => absurd $ i/=j $ inv (e.f_ret i) *> pmap e (fin_nat-inj $ NatSemiring.<=-antisymmetric i<=j j<=i) *> e.f_ret j
        }) (\lam k k/=j k/=i => p (e k) (\lam ek=i => k/=i $ inv (e.ret_f k) *> pmap e.ret ek=i) (\lam ek=j => k/=j $ inv (e.ret_f k) *> pmap e.ret ek=j)) *> pmap2 (x __ + x __) (e.f_ret j) (e.f_ret i) *> +-comm
      }
    }

  \lemma FinSum-pred {P : E -> \Prop} (P0 : P ) (P+ : \Pi {x y : E} -> P x -> P y -> P (x + y)) {J : FinSet} {a : J -> E} (p : \Pi (j : J) -> P (a j)) : P (AbMonoid.FinSum a)
    => \case FinSum_char a \with {
      | inP (e,q) => transportInv P q $ AddMonoid.BigSum-pred P0 P+ \lam i => p (e i)
    }
}
  \where {
    \use \coerce fromCMonoid (M : CMonoid) => \new AbMonoid M.E M.ide (M.*) M.ide-left M.ide-right M.*-assoc M.*-comm
    \use \coerce toCMonoid (M : AbMonoid) => \new CMonoid M.E M.zro (M.+) M.+-assoc M.zro-left M.zro-right M.+-comm
  }

\class CancelMonoid \extends Monoid
  | cancel_*-left (x : E) {y z : E} (p : x * y = x * z) : y = z
  | cancel_*-right (z : E) {x y : E} (p : x * z = y * z) : x = y

\class CancelCMonoid \extends CancelMonoid, CMonoid {
  | cancel_*-right z {x} {y} x*z=y*z => cancel_*-left z (*-comm *> x*z=y*z *> *-comm)

  \lemma divInv {x y : E} (xy|x : Monoid.LDiv (x * y) x) : Monoid.Inv y
    => CMonoid.divInv (cancel_*-left x) xy|x
}