\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/=)
\import Data.Or
\import Equiv
\import Equiv.Sigma
\import Equiv.Univalence
\import Function
\import Function.Meta
\import Logic.Unique
\import Logic
\import Logic.Classical
\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.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
    => 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

  \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 {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (p @) x right \in \Pi (x y : M) -> f (x * y) = f x * f y) : M = 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
    \where {
      \lemma cancel {M : Monoid} {x y z : M} (j : LInv x) (p : x * y = x * z) : y = z
        => y               ==< inv ide-left >==
           ide * y         ==< inv (pmap (`* y) j.inv-left) >==
           (j.inv * x) * y ==< *-assoc >==
           j.inv * (x * y) ==< pmap (j.inv *) p >==
           j.inv * (x * z) ==< inv *-assoc >==
           (j.inv * x) * z ==< pmap (`* z) j.inv-left >==
           ide * z         ==< ide-left >==
           z               `qed
    }

  -- | The type of right inverses of an element
  \record RInv \extends LDiv
    | elem => ide
    \where {
      \lemma cancel {M : Monoid} {x y z : M} (j : RInv z) (p : x * z = y * z) : x = y
        => x               ==< inv ide-right >==
           x * ide         ==< inv (pmap (x *) j.inv-right) >==
           x * (z * j.inv) ==< inv *-assoc >==
           (x * z) * j.inv ==< pmap (`* j.inv) p >==
           (y * z) * j.inv ==< *-assoc >==
           y * (z * j.inv) ==< pmap (y *) j.inv-right >==
           y * ide         ==< ide-right >==
           y               `qed
    }

  -- | 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 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)
    }
}

\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 \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)

  \sfunc FinSum {A : FinSet} (x : A -> E) : E
    => aux.
    \where {
      \lemma aux : \Sigma (r : E) (∃ (e : Equiv {Fin A.finCard} {A}) (BigSum (\lam j => x (e j)) = r))
        => TruncP.rec-set A.finEq _ aux
        \where
          \lemma aux (e e' : Equiv {Fin A.finCard} {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 $ transEquiv e' (symQEquiv e)
    }

  \lemma FinSum_char {A : FinSet} (x : A -> E) : ∃ (e : Equiv {Fin A.finCard} {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 : Equiv {Fin A.finCard} {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.finCard (\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 _, 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 => finCard {B (p. j)}) (\lam s => x (p. s., (f _). s.)) *>
                          inv (FinSum_char2 (unfold $ =-to-QEquiv (pmap Fin $ FinSum_char2 {NatSemiring} p.) `transEquiv` SigmaFin.aux `transEquiv` sigma-equiv p. (\lam j => (f _).)) *> pmap BigSum (exts $ (FinSum_char2 {NatSemiring} p., \lam j => idp)))
    }

  \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_Equiv {A B : FinSet} (e : Equiv {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.finCard { | finEq => TruncP.map B.finEq \lam e' => transEquiv e' (symQEquiv e)}
                 \in FinSum_char2 (transEquiv p. e) *> inv p. *> pmap {FinSet A} (FinSum {_} {__} _) (FinSet.levelProp A' A)
    }

  \lemma FinSum_Equiv2 {A B : FinSet} (e : Equiv {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))
    => \have 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) }
       \in FinSum_Equiv (later \new QEquiv {
         | 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
       }) *> FinSum_Or {_} {SigmaFin B \lam b => DecFin (decide {dec b})} {SigmaFin B \lam b => DecFin (decide {NotDecide (dec b)})} *>
             pmap2 (+) (FinSum_Equiv $ later $ Equiv.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.))
                       (FinSum_zro $ later \lam j => p j. \lam a q => j. $ inP (a,q)) *> zro-right

  \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 (transEquiv (OrFin.aux {A.finCard} {B.finCard}) (Or.Or_Equiv 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 : Equiv, 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
}