\import Algebra.Meta
\import Algebra.Pointed
\import Arith.Nat
\import Data.Array
\import Data.Fin (fsuc, fsuc/=)
\import Data.Or
\import Equiv
\import Equiv.Sigma
\import Equiv.Univalence
\import Function
\import Function.Meta
\import HLevel
\import Logic
\import Logic.Classical
\import Logic.Meta
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin
\import Set.Fin.Pigeonhole

\class Monoid \extends Pointed {
  | \infixl  * : E -> E -> E
  | ide-left {x : E} : ide * x = x
  | ide-right {x : E} : x * ide = x
  | *-assoc {x y z : E} : (x * y) * z = x * (y * z)

  \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_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 \elim n
    |  => ide-right *> inv ide-left
    | suc n => inv *-assoc *> pmap (`* a) pow-left

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

  \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

  \func op : Monoid E \cowith
    | ide => ide
    | * x y => y * x
    | ide-left => ide-right
    | ide-right => ide-left
    | *-assoc => inv *-assoc
} \where {
  \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 *) (Paths.inv *-assoc *> pmap (`* _) z|w.inv-right *> *-comm) *> Paths.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 => Paths.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 => Paths.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) ==< Paths.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) ==< Paths.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) ==< Paths.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
        => Paths.inv (*-assoc *> pmap (l *) l.inv-right) *> pmap (`* _) p *> l.inv-right

      \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 *> Paths.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) ==< Paths.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 *> Paths.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               ==< Paths.inv ide-left >==
           ide * y         ==< Paths.inv (pmap (`* y) j.inv-left) >==
           (j.inv * x) * y ==< *-assoc >==
           j.inv * (x * y) ==< pmap (j.inv *) p >==
           j.inv * (x * z) ==< Paths.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               ==< Paths.inv ide-right >==
           x * ide         ==< Paths.inv (pmap (x *) j.inv-right) >==
           x * (z * j.inv) ==< Paths.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 {
    \func op : Inv inv val \cowith
      | inv-left => inv-right
      | inv-right => inv-left
  } \where {
      \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 inv-isUnique {M : Monoid} (j j' : Inv {M}) (p : j.val = j'.val) : j.inv = j'.inv =>
        j.inv                 ==< Paths.inv ide-left >==
        ide * j.inv           ==< pmap (`* j.inv) (Paths.inv j'.inv-left) >==
        (j'.inv * j') * j.inv ==< pmap ((_ * __) * _) (Paths.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

      \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 *) (Paths.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 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)                 ==< Paths.inv ide-left >==
          ide * (y * (j.inv * x))         ==< pmap (`* (y * (j.inv * x))) (Paths.inv i.inv-left) >==
          (i.inv * x) * (y * (j.inv * x)) ==< *-assoc >==
          i.inv * (x * (y * (j.inv * x))) ==< pmap (i.inv *) (Paths.inv *-assoc) >==
          i.inv * ((x * y) * (j.inv * x)) ==< pmap (i.inv *) (Paths.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.op {a.}, inv $ pmap (_ *) a. *> inv *-assoc *> pmap (`* y) (Monoid.Inv.inv-left {a.}) *> 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 BigSum (l : Array E) => Big (+) zro l

  \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_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 NatSemiring.< 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, NatSemiring.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))

  \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.zro-left M.zro-right M.+-assoc
  }

\class CMonoid \extends Monoid {
  | *-comm {x y : E} : x * y = y * x
  \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 \elim n
    |  => inv ide-left
    | suc n => rewrite pow_*-comm equation

  \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_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 IsRegular (a : E) => \Pi {x y : E} -> a * x = a * y -> x = y

  \lemma LDiv_IsRegular {a b : E} (d : LDiv a b) (c : IsRegular b) : IsRegular 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 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)

  \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 p q r => equation {using (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 x = BigSum (\lam j => x (e j))) =>
    TruncP.map FinSum.aux. \lam t => (t., (\peval FinSum 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-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} (\lam i => finCard {B i}) 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 x 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 x (transEquiv p. e) *> inv p. *> pmap {FinSet A} (FinSum {_} {__} _) (FinSet.levelProp A' A)
    }

  \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 x (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-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.zro-left M.zro-right M.+-assoc 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
}