\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Arith.Nat
\import Data.Array
\import Data.Fin (fsuc/=, nat_fin_=)
\import Data.Or
\import Equiv
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Order.Biordered
\import Order.Lattice
\import Order.LinearOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin
\import Set.Fin.Instances

\class GradedCRing \extends CRing {
  | isHomogen : E -> Nat -> \Prop
  | homogen-zro {n : Nat} : isHomogen  n
  | homogen-+ {n : Nat} {a b : E} : isHomogen a n -> isHomogen b n -> isHomogen (a + b) n
  | homogen-* {n m : Nat} {a b : E} : isHomogen a n -> isHomogen b m -> isHomogen (a * b) (n Nat.+ m)
  | homogen-decomp (x : E) : ∃ (l : Array E) (\Pi (n : Fin l.len) -> isHomogen (l n) n) (BigSum l = x)
  | homogen-unique (l : Array E) : (\Pi (n : Fin l.len) -> isHomogen (l n) n) -> BigSum l =  -> ∀ (x : l) (x = )

  \func isHomogenArray (l : Array E) => \Pi (n : Fin l.len) -> isHomogen (l n) n

  \lemma homogen-ide : isHomogen  
    => \case homogen-decomp  \with {
      | inP (nil, lh, l=1) => transport (isHomogen __ ) l=1 homogen-zro
      | inP (x0 :: l, lh, l=1) =>
        \have | lj=x0lj {j} : l j = x0 * l j =>
                \let | l1 => replicate (suc j) 
                     | l' => l1 ++ map (l j *) (x0 :: l)
                     | lj=l' : l j = BigSum l' => inv (pmap (_ *) l=1 *> ide-right) *> BigSum-ldistr {_} {_} {x0 :: l} *> inv zro-left *> pmap (+ _) (inv $ BigSum_zro {_} {l1} \lam _ => idp) *> inv (BigSum_++ {_} {l1})
                \in \case homogenSum-unique {_} {l'} (\lam i => \case ++.split-index {_} {l1} i \with {
                  | inl (i',i_i') => transportInv (\lam r => isHomogen (l' r) _) (fin_nat-inj i_i') $ transportInv (isHomogen __ i) (++.++_index-left i') homogen-zro
                  | inr (i',i_i') => transportInv (\lam r => isHomogen (l' r) _) (fin_nat-inj i_i') $ transportInv (isHomogen __ i) ++.++_index-right $ transportInv (isHomogen _) (later $ i_i' *> pmap suc ++.index-right-nat) $ homogen-* (lh (suc j)) (lh i')
                }) (transport (isHomogen __ _) lj=l' (lh (suc j))) \with {
                  | inl (j',q,j'_j) => lj=l' *> q *> pmap ((++) (replicate (suc j) zro) _ __) {j'} {++.index-right {_} {replicate (suc j) zro} } (fin_nat-inj $ j'_j *> pmap suc (inv ++.index-right-nat)) *> ++.++_index-right *> *-comm
                  | inr l'=0 => lj=l' *> l'=0 *> inv (pmap (_ *) (lj=l' *> l'=0) *> zro_*-right)
                }
              | x0lj=0 {j} : x0 * l j =  => homogen-unique (negative x0 + x0 * x0 :: map (x0 *) l) (\case \elim __ \with {
                |  => homogen-+ (homogen-negative (lh )) $ homogen-* (lh ) (lh )
                | suc i => homogen-* (lh ) (lh (suc i))
              }) (+-assoc *> +-comm *> toZero (inv (BigSum-ldistr {_} {_} {x0 :: l}) *> pmap (_ *) l=1 *> ide-right)) (suc j)
        \in transportInv (isHomogen __ ) (inv l=1 *> pmap (_ +) (BigSum_zro \lam j => lj=x0lj *> x0lj=0) *> zro-right) (lh )
    }

  \lemma homogen-negative {n : Nat} {x : E} (xh : isHomogen x n) : isHomogen (negative x) n
    => \case homogen-decomp (negative x) \with {
      | inP (l,lh,l=-x) => \case LinearOrder.dec<_<= n l.len \with {
        | inl n<l =>
          \have | l' => \new Array E l.len \lam j => \case decideEq n j \with {
                          | yes _ => l j + x
                          | no _ => l j
                        }
                | ln+x=0 => rewrite (decideEq=_reduce $ inv toFin=id) in homogen-unique l' (\lam j => mcases \with {
                    | yes n=j => homogen-+ (lh j) $ transport (isHomogen x) n=j xh
                    | no _ => lh j
                  }) (cancel-right (negative (BigSum l)) $ pmap (_ +) BigSum_negative *> inv (BigSum_+ {_} {_} {l'}) *>
                    BigSum-unique {_} {\new Array E l.len \lam j => l' j - l j} (toFin n n<l)
                      (\lam j n/=j => rewrite (decideEq/=_reduce \lam n=j => n/=j $ fin_nat-inj $ toFin=id *> n=j) negative-right) *>
                    rewrite (decideEq=_reduce $ inv toFin=id) equation.abGroup *> inv negative-isInv *> pmap negative (inv l=-x) *> inv zro-left) (toFin n n<l)
          \in transport2 isHomogen (fromZero $ pmap (_ +) negative-isInv *> ln+x=0) toFin=id (lh _)
        | inr n>=l =>
          \have x=0 => inv ++.++_index-right *> inv ++.++_index-right *> homogen-unique _ (homogen-++ {_} {l} {replicate (n -' l.len)  ++ (x :: nil)} lh \lam j => \case ++.split-index j \with {
              | inl (j1,j_j1) => transportInv (isHomogen __ _) (later $ rewrite j_j1 $ ++.++_index-left j1) homogen-zro
              | inr (,j_0) => transport2 isHomogen (later $ rewrite j_0 $ inv $ ++.++_index-right) (inv $ pmap {Nat} (_ Nat.+) (j_0 *> ++.index-right-nat) *> <=_exists n>=l) xh
            }) (BigSum_++ *> pmap2 (+) l=-x (BigSum_++ *> pmap2 (+) (BigSum_zro \lam _ => idp) zro-right *> zro-left) *> negative-left) (++.index-right $ ++.index-right )
          \in transportInv (isHomogen __ n) (pmap negative x=0 *> negative_zro) homogen-zro
      }
    }

  \lemma homogen-pow {a : E} {n : Nat} (ah : isHomogen a n) {m : Nat} : isHomogen (pow a m) (n Nat.* m) \elim m
    |  => homogen-ide
    | suc m => homogen-* (homogen-pow ah) ah

  \lemma homogen-BigSum {l : Array E} {n : Nat} (p : ∀ (a : l) (isHomogen a n)) : isHomogen (BigSum l) n \elim l
    | nil => homogen-zro
    | a :: l => homogen-+ (p ) (homogen-BigSum (\lam j => p (suc j)))

  \lemma homogen-FinSum {J : FinSet} {a : J -> E} {n : Nat} (p : \Pi (j : J) -> isHomogen (a j) n) : isHomogen (FinSum a) n
    => \case FinSum_char a \with {
      | inP (e,q) => transportInv (isHomogen __ n) q $ homogen-BigSum \lam j => p (e j)
    }

  \func IsHomogen (a : E) : \Prop
    => ∃ (n : Nat) (isHomogen a n)

  \lemma IsHomogen_ide : IsHomogen 
    => inP (, homogen-ide)

  \lemma IsHomogen_* {a b : E} (ah : IsHomogen a) (bh : IsHomogen b) : IsHomogen (a * b) \elim ah, bh
    | inP (n,ah), inP (m,bh) => inP (_, homogen-* ah bh)

  \lemma IsHomogen_pow {a : E} (ah : IsHomogen a) {k : Nat} : IsHomogen (pow a k) \elim ah
    | inP (n,ah) => inP (_, homogen-pow ah)

  \lemma homogen-similar {l l' : Array E} (lh : isHomogenArray l) (l'h : isHomogenArray l') (p : BigSum l = BigSum l') : Similar l l'
    => diff=0->similar $ homogen-unique (diff l l') (diff-homogen l l'  lh l'h) (diff-sum l l' *> toZero p)
    \where {
      \func diff (l l' : Array E) : Array E \elim l, l'
        | nil, l' => map negative l'
        | a :: l, nil => a :: l
        | a :: l, a' :: l' => a - a' :: diff l l'

      \lemma diff=0->similar {l l' : Array E} (p : \Pi (j : Fin (DArray.len {diff l l'})) -> diff l l' j = ) : Similar l l' \elim l, l'
        | nil, nil => nil-nil-similar
        | nil, a :: l' => nil-::-similar (inv negative-isInv *> pmap negative (p ) *> negative_zro) $ diff=0->similar \lam j => p (suc j)
        | a :: nil, nil => ::-nil-similar (p ) nil-nil-similar
        | a :: a' :: l, nil => ::-nil-similar (p ) $ diff=0->similar \lam j => p (suc j)
        | a :: l, a' :: l' => ::-::-similar (fromZero $ p ) $ diff=0->similar \lam j => p (suc j)

      \lemma diff-sum (l l' : Array E) : BigSum (diff l l') = BigSum l - BigSum l' \elim l, l'
        | nil, l' => inv $ zro-left *> BigSum_negative
        | a :: l, nil => simplify
        | a :: l, a' :: l' => equation {usingOnly (diff-sum l l')}

      \lemma diff-homogen (l l' : Array E) (k : Nat)
                          (lh : \Pi (j : Fin l.len) -> isHomogen (l j) (k Nat.+ j))
                          (l'h : \Pi (j : Fin l'.len) -> isHomogen (l' j) (k Nat.+ j))
                          (j : Fin (DArray.len {diff l l'})) : isHomogen (diff l l' j) (k Nat.+ j) \elim l, l', j
        | nil, a :: l',  => homogen-negative (l'h )
        | nil, a :: l', suc j => homogen-negative (l'h (suc j))
        | a :: l, nil,  => lh 
        | a :: a' :: l, nil, suc j => diff-homogen (a' :: l) nil (suc k) (\lam j => lh (suc j)) (\case __) j
        | a :: l, a' :: l',  => homogen-+ (lh ) (homogen-negative (l'h ))
        | a :: l, a' :: l', suc j => diff-homogen l l' (suc k) (\lam j => lh (suc j)) (\lam j => l'h (suc j)) j
    }

  \func degree-unique {a : E} {n m : Nat} (ahn : isHomogen a n) (ahm : isHomogen a m) : Or (a = ) (n = m)
    => \case decideEq n m \with {
      | yes e => inr e
      | no q => inl $ rewrite (decideEq=_reduce $ inv $ fin-inc.char_nat {suc m} n) in
          \let l => array2 n m a (negative a)
          \in homogen-unique l (\lam j => mcases \with {
            | yes p, d => rewriteI p ahn
            | no n1, yes p => rewriteI p (homogen-negative ahm)
            | no n1, no n2 => homogen-zro
          }) (sum-lem2 {_} {l} (fin-inc {suc n} {suc m} (n Nat.mod suc n)) (fin-inc-right {suc n} (m Nat.mod suc m))
                (\lam p => q $ inv (fin-inc.char_nat {suc m} n) *> p *> fin-inc-right.char_nat {suc n} m)
                (\lam k p1 p2 => rewrite (decideEq/=_reduce \lam p => p1 $ fin_nat-inj $ inv $ fin-inc.char_nat {suc m} n *> p, decideEq/=_reduce \lam p => p2 $ fin_nat-inj $ inv $ fin-inc-right.char_nat {suc n} m *> p) idp)
              *> rewrite (decideEq=_reduce $ inv $ fin-inc.char_nat {suc m} n, decideEq=_reduce $ inv $ fin-inc-right.char_nat {suc n} m, decideEq/=_reduce \lam p => q $ p *> fin-inc-right.char_nat {suc n} m) negative-right) (fin-inc {_} {suc m} (n Nat.mod suc n))
    } \where {
      \func array2 (n m : Nat) (a b : E) => \new Array E (suc n Nat.+ suc m) \lam j => \case decideEq n j, decideEq m j \with {
        | yes _, _ => a
        | no _, yes _ => b
        | no _, no _ => 
      }

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

      \lemma sum-lem2 {l : Array E} (i j : Fin l.len) (i/=j : i /= j) (c : \Pi (k : Fin l.len) -> k /= i -> k /= j -> l k = ) : BigSum l = l i + l j \elim l, i, j
        | nil, i, _ => \case i
        | a :: l, ,  => \case i/=j idp
        | a :: l, , suc j => pmap (a +) (sum-lem1 j \lam k d => c (suc k) (\case __) (fsuc/= d))
        | a :: l, suc i,  => pmap (a +) (sum-lem1 i \lam k d => c (suc k) (fsuc/= d) (\case __)) *> +-comm
        | a :: l, suc i, suc j => pmap (+ _) (c  (\case __) (\case __)) *> zro-left *> sum-lem2 i j (\lam p => i/=j \lam i => suc (p i)) (\lam k d1 d2 => c (suc k) (fsuc/= d1) (fsuc/= d2))
  }

  \func degree-unique2 {a b c : E} {n m k : Nat} (p : a = b + c) (ah : isHomogen a n) (bh : isHomogen b m) (ch : isHomogen c k) : Or (Or (b = ) (c = )) (m = k)
    => \case decideEq m k \with {
      | yes m=k => inr m=k
      | no m/=k => \let | l => degree-unique.array2 m k b c
                        | s => homogen-similar {_} {l} {replicate n zro ++ a :: nil} (\lam j => mcases \with {
                            | yes e, d => rewriteI e bh
                            | no _, yes e => rewriteI e ch
                            | no n1, no n2 => homogen-zro
                          }) (homogen-++ (\lam j => homogen-zro) $ later \lam () => ah) $
                          degree-unique.sum-lem2 {_} {l} (fin-inc {_} {suc k} (m Nat.mod suc m)) (fin-inc-right {suc m} (k Nat.mod suc k))
                              (\lam p => m/=k $ inv (fin-inc.char_nat {suc k} m) *> p *> fin-inc-right.char_nat {suc m} k)
                              (\lam l p1 p2 => rewrite (decideEq/=_reduce \lam p => p1 $ fin_nat-inj $ inv $ fin-inc.char_nat {suc k} m *> p, decideEq/=_reduce \lam p => p2 $ fin_nat-inj $ inv $ fin-inc-right.char_nat {suc m} k *> p) idp)
                          *> rewrite (decideEq=_reduce $ inv $ fin-inc.char_nat {suc k} m, decideEq=_reduce $ inv $ fin-inc-right.char_nat {suc m} k, decideEq/=_reduce \lam p => m/=k $ p *> fin-inc-right.char_nat {suc m} k) (inv p) *> inv (BigSum_++ *> pmap (+ _) BigSum_replicate0 *> simplify)
                   \in \case decideEq n m \with {
                     | yes n=m => cases (decideEq m (fin-inc-right {suc m} (k Nat.mod suc k)), decideEq k (fin-inc-right {suc m} (k Nat.mod suc k)), similar-unique l a n s (fin-inc-right {suc m} (k Nat.mod suc k)) \lam p => m/=k $ inv n=m *> p *> fin-inc-right.char_nat {suc m} k) \with {
                         | yes e, _, t => inl (inl t)
                         | no n1, yes e, t => inl (inr t)
                         | no _, no c, t => absurd $ c $ inv $ fin-inc-right.char_nat {suc m} k
                       }
                     | no n/=m => inl $ inl $ rewrite (decideEq=_reduce $ inv $ fin-inc.char_nat {suc k} m) in similar-unique l a n s (fin-inc {_} {suc k} (m Nat.mod suc m)) \lam p => n/=m $ p *> fin-inc.char_nat {suc k} m
                   }
    }
    \where {
      \lemma similar-unique (l : Array E) (a : E) (n : Nat) (s : Similar l (replicate n zro ++ a :: nil)) (j : Fin l.len) (n/=j : n /= j) : l j =  \elim l, n, s, j
        | a' :: l, , ::-::-similar p s,  => absurd (n/=j idp)
        | a' :: l, , ::-::-similar p s, suc j => similar-nil s j
        | a' :: l, suc n, ::-::-similar p s,  => p
        | a' :: l, suc n, ::-::-similar p s, suc j => similar-unique l a n s j \lam q => n/=j (pmap suc q)
    }

  \func homogenSum-unique {l : Array E} (lh : isHomogenArray l) {n : Nat} (h : isHomogen (BigSum l) n)
    : Or (\Sigma (j : Fin l.len) (BigSum l = l j) (j = {Nat} n)) (BigSum l = )
    => \case similar-eq (homogen-similar {_} {replicate n zro ++ BigSum l :: nil} (homogen-++ (\lam j => homogen-zro) $ later \lam () => h) lh $
              BigSum_++ *> pmap2 (+) BigSum_replicate0 zro-right *> zro-left) (++.index-right ) \with {
         | inl r => inl (r., inv ++.++_index-right *> r., r. *> ++.index-right-nat)
         | inr r => inr (inv ++.++_index-right *> r)
       }

  \lemma homogen-++ {l l' : Array E} (lh : isHomogenArray l) (l'h : \Pi (j : Fin l'.len) -> isHomogen (l' j) (l.len Nat.+ j)) : isHomogenArray (l ++ l')
    => aux  lh l'h
    \where
      \lemma aux {l l' : Array E} (n : Nat)
                 (lh : \Pi (j : Fin l.len) -> isHomogen (l j) (n Nat.+ j))
                 (l'h : \Pi (j : Fin l'.len) -> isHomogen (l' j) (n Nat.+ l.len Nat.+ j))
                 (j : Fin (DArray.len {l ++ l'}))
        : isHomogen ((++) l l' j) (n Nat.+ j) \elim l, j
        | nil, j => l'h j
        | a :: l,  => lh 
        | a :: l, suc j => aux (suc n) (\lam j => lh (suc j)) l'h j

  \lemma homogen-factor {a b : E} (a|b : Monoid.LDiv a b) (bh : IsHomogen b) (ah : IsHomogen a)
    : ∃ (c : E) (k : Nat) (isHomogen c k) (b = a * c) \elim bh, ah
    | inP (n,bh), inP (m,ah) => TruncP.map (homogen-decomp a|b.inv) \lam (l,lh,+l=c) => aux n m  lh $ homogen-similar
         (homogen-++ (\lam j => homogen-zro) $ later \lam () => bh)
         (homogen-++ (\lam j => homogen-zro) $ later \lam j => homogen-* ah (lh j))
         (BigSum_++ *> pmap (+ _) BigSum_replicate0 *> later (simplify $ inv a|b.inv-right *> pmap (a *) (inv +l=c) *> BigSum-ldistr) *> inv (BigSum_++ *> pmap (+ _) BigSum_replicate))
    \where {
      \func aux {a b : E} (s t n : Nat) {l : Array E} (lh : \Pi (j : Fin l.len) -> isHomogen (l j) (n Nat.+ j)) (p : Similar (replicate s zro ++ b :: nil) (replicate t zro ++ map (a *) l))
        : \Sigma (c : E) (k : Nat) (isHomogen c k) (b = a * c) \elim s, t, l, p
        | , , nil, ::-nil-similar idp _ => (, , homogen-zro, inv zro_*-right)
        | , , c :: l, ::-::-similar p _ => (c, n, lh , p)
        | , suc t, l, ::-::-similar idp _ => (, , homogen-zro, inv zro_*-right)
        | suc s, , nil, ::-nil-similar _ q => aux s  n lh q
        | suc s, , c :: l, ::-::-similar _ q => aux s  (suc n) (\lam j => lh (suc j)) q
        | suc s, suc t, l, ::-::-similar _ q => aux s t n lh q
    }

  \lemma homogen-factor2 {a1 a2 b c d : E} (b=ac : b = a1 * c + a2 * d) {n m1 m2 : Nat} (bh : isHomogen b n) (a1h : isHomogen a1 m1) (a2h : isHomogen a2 m2)
    : ∃ (c' d' : E) (k1 k2 : Nat) (isHomogen c' k1) (isHomogen d' k2) (b = a1 * c' + a2 * d')
    => \case homogen-decomp c, homogen-decomp d \with {
      | inP (l1,l1h,+l1=c1), inP (l2,l2h,+l2=c2) => inP $ aux n m1 m2   l1h l2h $ homogen-similar
          (homogen-++ (\lam j => homogen-zro) $ later \lam () => bh)
          (homogen-sum  (homogen-++ (\lam j => homogen-zro) (\lam j => later $ homogen-* a1h (l1h j))) (homogen-++ (\lam j => homogen-zro) (\lam j => later $ homogen-* a2h (l2h j))))
          $ BigSum_++ *> pmap (+ _) BigSum_replicate0 *> simplify b=ac *>
            inv (BigSum_sum *> pmap2 (+) (BigSum_++ *> pmap (+ _) BigSum_replicate0 *> zro-left) (BigSum_++ *> pmap (+ _) BigSum_replicate0 *> zro-left) *> pmap2 (+) (inv BigSum-ldistr *> pmap (a1 *) +l1=c1) (inv BigSum-ldistr *> pmap (a2 *) +l2=c2))
    }
    \where {
      \func sum (l l' : Array E) : Array E \elim l, l'
        | nil, l' => l'
        | a :: l, nil => a :: l
        | a :: l, a' :: l' => a + a' :: sum l l'

      \lemma sum_nil {l : Array E} : sum l nil = l \elim l
        | nil => idp
        | a :: l => idp

      \lemma BigSum_sum {l l' : Array E} : BigSum (sum l l') = BigSum l + BigSum l' \elim l, l'
        | nil, nil => inv zro-left
        | nil, a :: l => inv zro-left
        | a :: l, nil => inv zro-right
        | a :: l, a' :: l' => pmap (_ +) BigSum_sum *> equation

      \lemma homogen-sum {l l' : Array E} (n : Nat)
                         (lh : \Pi (j : Fin l.len) -> isHomogen (l j) (n Nat.+ j))
                         (l'h : \Pi (j : Fin l'.len) -> isHomogen (l' j) (n Nat.+ j))
                         (j : Fin (DArray.len {sum l l'}))
        : isHomogen (sum l l' j) (n Nat.+ j) \elim l, l', j
        | nil, a :: l,  => l'h 
        | nil, a :: l, suc j => l'h (suc j)
        | a :: l, nil,  => lh 
        | a :: l, nil, suc j => lh (suc j)
        | a :: l, a' :: l',  => homogen-+ (lh ) (l'h )
        | a :: l, a' :: l', suc j => homogen-sum (suc n) (\lam j => lh (suc j)) (\lam j => l'h (suc j)) j

      \func aux {a1 a2 b : E} (s t1 t2 n1 n2 : Nat) {l1 l2 : Array E}
                (l1h : \Pi (j : Fin l1.len) -> isHomogen (l1 j) (n1 Nat.+ j))
                (l2h : \Pi (j : Fin l2.len) -> isHomogen (l2 j) (n2 Nat.+ j))
                (p : Similar (replicate s zro ++ b :: nil) (sum (replicate t1 zro ++ map (a1 *) l1) (replicate t2 zro ++ map (a2 *) l2)))
        : \Sigma (c1 c2 : E) (k1 k2 : Nat) (isHomogen c1 k1) (isHomogen c2 k2) (b = a1 * c1 + a2 * c2) \elim s, t1, t2, l1, l2, p
        | , , , nil, nil, ::-nil-similar p _ => (, , , , homogen-zro, homogen-zro, p *> simplify)
        | , , , nil, c2 :: l2, ::-::-similar p q => (, c2, , n2, homogen-zro, l2h , p *> simplify)
        | , , , c1 :: l1, nil, ::-::-similar p q => (c1, , n1, , l1h , homogen-zro, p *> simplify)
        | , , , c1 :: l1, c2 :: l2, ::-::-similar p _ => (c1, c2, n1, n2, l1h , l2h , p)
        | , , suc t2, nil, _, ::-::-similar p _ => (, , , , homogen-zro, homogen-zro, p *> simplify)
        | , , suc t2, c1 :: l1, _, ::-::-similar p q => (c1, , n1, , l1h , homogen-zro, p *> simplify)
        | , suc t1, , _, nil, ::-::-similar p q => (, , , , homogen-zro, homogen-zro, p *> simplify)
        | , suc t1, , _, c2 :: l2, ::-::-similar p q => (, c2, , n2, homogen-zro, l2h , p *> simplify)
        | , suc t1, suc t2, l1, l2, ::-::-similar p q => (, , , , homogen-zro, homogen-zro, p *> simplify)
        | suc s, , , nil, nil, ::-nil-similar _ q => aux s   n1 n2 l1h l2h q
        | suc s, , , nil, c2 :: l2, ::-::-similar _ q => aux s   n1 (suc n2) l1h (\lam j => l2h (suc j)) q
        | suc s, , , c1 :: l1, nil, ::-::-similar _ q => aux s   (suc n1) n2 (\lam j => l1h (suc j)) l2h (rewrite sum_nil q)
        | suc s, , , c1 :: l1, c2 :: l2, ::-::-similar _ q => aux s   (suc n1) (suc n2) (\lam j => l1h (suc j)) (\lam j => l2h (suc j)) q
        | suc s, , suc t2, nil, l2, ::-::-similar _ q => aux s  t2 n1 n2 l1h l2h q
        | suc s, , suc t2, c1 :: l1, l2, ::-::-similar _ q => aux s  t2 (suc n1) n2 (\lam j => l1h (suc j)) l2h q
        | suc s, suc t1, , l1, nil, ::-::-similar _ q => aux s t1  n1 n2 l1h l2h (rewrite sum_nil q)
        | suc s, suc t1, , l1, c2 :: l2, ::-::-similar _ q => aux s t1  n1 (suc n2) l1h (\lam j => l2h (suc j)) q
        | suc s, suc t1, suc t2, l1, l2, ::-::-similar _ q => aux s t1 t2 n1 n2 l1h l2h q
    }

  \lemma FinSum-homogen {J : FinSet} {a : J -> E} (p : \Pi (j : J) -> \Sigma (n : Nat) (isHomogen (a j) n)) : FinSum a = BigSum array
    => FinSum_Equiv (later \new QEquiv {
      | f s => s..
      | ret j => (finMod (p j)., (j, inv $ mod_< $ FinJoin-cond _ <∘r id<suc))
      | ret_f s => exts (nat_fin_= $ mod_< (FinJoin-cond s.. <∘r id<suc) *> s.., idp)
      | f_sec j => idp
    }) *> inv (FinSum-double-dep (\lam i => SigmaFin J \lam j => DecFin (decideEq (p j). i)) {\lam s => a s..}) *> FinSum=BigSum {_} {suc $ FinJoin (\lam j => (p j).)}
    \where {
      \func array => \new Array E (suc $ FinJoin (\lam j => (p j).)) \lam i => FinSum {_} {SigmaFin J \lam j => DecFin (decideEq (p j). i)} (\lam k => a k.)

      \lemma array-homogen : isHomogenArray array
        => \lam n => homogen-FinSum $ later \lam j => transport (isHomogen _) j. (p j.).
    }

  \lemma sum-decomp (l : Array (\Sigma E E)) (c : \Pi (i : Fin l.len) -> ∃ (n : Nat) (isHomogen (l i). n))
    : ∃ (N : Nat) (f : \Pi (n : Fin N) -> \Sigma (J : FinSet.{}) (g : J -> E) (\Pi (j : J) -> \Sigma (n : Nat) (isHomogen (g j) n)) (h : J -> Fin l.len) (\Pi (j : J) -> isHomogen (g j * (l (h j)).) n))
        (BigSum (map (\lam s => s. * s.) l) = BigSum (\lam n => FinSum (\lam j => (f n). j * (l ((f n). j)).)))
    => \let | (inP c') => FinSet.finiteAC c
            | (inP d) => FinSet.finiteAC (\lam i => homogen-decomp (l i).)
            | p k : _ => later $ (k. Nat.+ (c' k.)., homogen-* ((d k.). k.) (c' k.).)
            | q => path (\lam i => BigSum (\lam i' => inv (FinSum=BigSum *> (d i').) i * (l i').)) *> inv FinSum=BigSum *>
                   pmap FinSum (ext \lam j => FinSum-rdistr) *> FinSum-double-dep (\lam i => FinFin (DArray.len {(d i).})) *> FinSum-homogen p
       \in inP (suc _, \lam n => (SigmaFin (SigmaFin (FinFin l.len) (\lam i => FinFin (DArray.len {(d i).}))) (\lam k => DecFin (decideEq (p k). n)), \lam k => (d k..). k.., \lam k => (k.., (d k..). k..), __.., \lam k => transport (isHomogen _) k. (p k.).), q)
} \where {
  \open BottomJoinSemilattice

  \data Similar {A : AddPointed} (l l' : Array A) \elim l, l'
    | nil, nil => nil-nil-similar
    | nil, a :: l' => nil-::-similar (a = ) (Similar nil l')
    | a :: l, nil => ::-nil-similar (a = ) (Similar l nil)
    | a :: l, a' :: l' => ::-::-similar (a = a') (Similar l l')

  \lemma similar-nil {A : AddPointed} {l : Array A} (s : Similar l nil) (j : Fin l.len) : l j =  \elim l, s, j
    | a :: l, ::-nil-similar p s,  => p
    | a :: l, ::-nil-similar p s, suc j => similar-nil s j

  \func similar-eq {A : AddPointed} {l l' : Array A} (s : Similar l l') (j : Fin l.len)
    : Or (\Sigma (i : Fin l'.len) (l j = l' i) (i = {Nat} j)) (l j = ) \elim l, l', s, j
    | a :: l, nil, ::-nil-similar p s,  => inr p
    | a :: l, nil, ::-nil-similar p s, suc j => \case similar-eq s j \with {
      | inl r => \case r.
      | inr r => inr r
    }
    | a :: l, a' :: l', ::-::-similar p s,  => inl (, p, idp)
    | a :: l, a' :: l', ::-::-similar p s, suc j => \case similar-eq s j \with {
      | inl r => inl (suc r., r., pmap suc r.)
      | inr r => inr r
    }
}