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

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

\lemma binom_< {n m : Nat} (p : n < m) : binom n m = 0 \elim n, m, p
| 0, 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
| 0 => 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))))
}