\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ring
\import Algebra.Semiring
\import Arith.Int
\import Arith.Nat
\import Data.Array
\import Order.StrictOrder
\import Paths
\open Monoid (pow)
\open AddMonoid (BigSum)

\func binom (n i : Nat) : Nat
  | _,  => 
  | , _ => 
  | suc n, suc i => binom n i + binom n (suc i)
  \where {
    \lemma binom_0 {n : Nat} : binom n  =  \elim n
      |  => idp
      | suc n => idp

    \lemma binom_< {n m : Nat} (p : n < m) : binom n m =  \elim n, m, p
      | , suc m, _ => idp
      | suc n, suc m, NatSemiring.suc<suc n<m => pmap2 (+) (binom_< n<m) (binom_< (n<m <∘ id<suc))

    \lemma expansion {R : CRing} (x y : R) (n : Nat) : pow (x + y) n = BigSum (\new Array R (suc n) (\lam i => natCoef (binom n i) * (pow x i * pow y (iabs (n Nat.- i))))) \elim n
      |  => equation
      | suc n => \let | xy i => pow x (suc i) * pow y (iabs (n Nat.- i))
                      | cxy (i : Fin (suc n)) => natCoef (binom n i) * (pow x i * pow y (iabs (n Nat.- i)))
                      | t1 : pow (x + y) n * x = BigSum (\new Array R (suc n) (\lam i => natCoef (binom n i) * xy i))
                           => pmap (`* x) (expansion x y n) *> R.BigSum-rdistr {\new Array R.E (suc n) cxy} *>
                              path (\lam j => BigSum (\new Array R (suc n) (\lam i => (equation : cxy i * x = natCoef (binom n i) * xy i) @ j)))
                      | t2 : pow (x + y) n * y = BigSum (\new Array R (suc (suc n)) (\lam i => natCoef (binom n i) * (pow x i * pow y (iabs (suc n Nat.- i)))))
                           => pmap (`* y) (expansion x y n) *> R.BigSum-rdistr {\new Array R (suc n) cxy} *>
                              path (\lam j => BigSum (\new Array R (suc n) (\lam i => ((equation : cxy i * y = natCoef (binom n i) * (pow x i * pow y (suc (iabs (n Nat.- i))))) *>
                                pmap (\lam m => natCoef (binom n i) * (pow x i * pow y m)) (inv (iabs_-_suc (<_suc_<= (fin_< i))))) @ j))) *>
                              inv (pmap (_ +) (pmap (`* _) (pmap natCoef (binom_< (transportInv (n <) (mod_< id<suc) id<suc)) *> natCoefZero) *> zro_*-left) *> zro-right) *>
                              inv (R.BigSum_suc {suc n} {\new Array R (suc (suc n)) (\lam i => natCoef (binom n i) * (pow x i * pow y (iabs (suc n Nat.- i))))})
                 \in ldistr *> pmap2 (+) t1 (t2 *> pmap (natCoef __ * _ + _) binom_0) *> +-comm *> +-assoc *> pmap (_ +) +-comm *>
                     inv (pmap (_ +) (R.BigSum_+ {suc n} {mkArray (\lam i => natCoef (binom n i) * xy i)} {mkArray (\lam i => natCoef (binom n (suc i)) * xy i)})) *>
                     inv (path (\lam j => _ + BigSum (\new Array R (suc n) (\lam i => (pmap (`* xy i) (Semiring.natCoef_+ (binom n i) (binom n (suc i))) *> rdistr) @ j))))
  }