matita-arithmetics-binomial.agda

open import Agda.Primitive
open import matita-arithmetics-primes
open import matita-arithmetics-div-and-mod
open import matita-arithmetics-factorial
open import matita-arithmetics-bigops
open import matita-arithmetics-sigma-pi
open import matita-basics-bool
open import matita-basics-logic
open import matita-arithmetics-exp
open import matita-arithmetics-nat
bc : (X-n : nat) -> (X-k : nat) -> nat
bc = λ (n : nat) -> λ (k : nat) -> div (fact n) (times (fact k) (fact (minus n k)))

bceq : (n : nat) -> (k : nat) -> eq lzero nat (bc n k) (div (fact n) (times (fact k) (fact (minus n k))))
bceq = λ (n : nat) -> λ (k : nat) -> refl lzero nat (bc n k)

bc-n-n : (n : nat) -> eq lzero nat (bc n n) (S O)
bc-n-n = λ (n : nat) -> eq-ind-r lzero lzero nat (div (fact n) (times (fact n) (fact (minus n n)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (fact n) (times (fact n) (fact (minus n n))))) -> eq lzero nat x (S O)) (eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> eq lzero nat (div (fact n) (times (fact n) (fact x-1))) (S O)) (eq-ind lzero lzero nat (fact n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (fact n) x-1) -> eq lzero nat (div (fact n) x-1) (S O)) (div-n-n (fact n) (le-1-fact n)) (times (fact n) (S O)) (times-n-1 (fact n))) (minus n n) (minus-n-n n)) (bc n n) (bceq n n)

bc-n-O : (n : nat) -> eq lzero nat (bc n O) (S O)
bc-n-O = λ (n : nat) -> eq-ind-r lzero lzero nat (div (fact n) (times (fact O) (fact (minus n O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (fact n) (times (fact O) (fact (minus n O))))) -> eq lzero nat x (S O)) (eq-ind lzero lzero nat n (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat n x-1) -> eq lzero nat (div (fact n) (times (fact O) (fact x-1))) (S O)) (injective-plus-r n (div (fact n) (times (fact O) (fact n))) (S O) (rewrite-l lzero lzero nat (bc n n) (λ (X-- : nat) -> eq lzero nat (plus n (div (fact n) (times (fact O) (fact n)))) (plus n X--)) (rewrite-r lzero lzero nat (times (fact n) (fact O)) (λ (X-- : nat) -> eq lzero nat (plus n (div (fact n) X--)) (plus n (bc n n))) (rewrite-l lzero lzero nat (bc n n) (λ (X-- : nat) -> eq lzero nat (plus n X--) (plus n (bc n n))) (refl lzero nat (plus n (bc n n))) (div (fact n) (times (fact n) (fact O))) (rewrite-r lzero lzero nat (minus n n) (λ (X-- : nat) -> eq lzero nat (bc n n) (div (fact n) (times (fact n) (fact X--)))) (bceq n n) O (minus-n-n n))) (times (fact O) (fact n)) (commutative-times (fact O) (fact n))) (S O) (bc-n-n n))) (minus n O) (minus-n-O n)) (bc n O) (bceq n O)

fact-minus : (n : nat) -> (k : nat) -> (X-- : lt k n) -> eq lzero nat (times (fact (minus n (S k))) (minus n k)) (fact (minus n k))
fact-minus = λ (n : nat) -> λ (k : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : lt k X--) -> eq lzero nat (times (fact (minus X-- (S k))) (minus X-- k)) (fact (minus X-- k))) (λ (ltO : lt k O) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat (times (fact (minus O (S k))) (minus O k)) (fact (minus O k))) (absurd lzero (le (S k) O) ltO (not-le-Sn-O k))) (λ (l : nat) -> λ (ltl : lt k (S l)) -> eq-ind-r lzero lzero nat (S (minus l k)) (λ (x : nat) -> λ (X-- : eq lzero nat x (S (minus l k))) -> eq lzero nat (times (fact (minus (S l) (S k))) x) (fact x)) (rewrite-r lzero lzero nat (minus l k) (λ (X-- : nat) -> eq lzero nat (times (fact X--) (S (minus l k))) (fact (S (minus l k)))) (rewrite-l lzero lzero nat (plus (fact (minus l k)) (times (fact (minus l k)) (minus l k))) (λ (X-- : nat) -> eq lzero nat X-- (fact (S (minus l k)))) (rewrite-r lzero lzero nat (times (minus l k) (fact (minus l k))) (λ (X-- : nat) -> eq lzero nat (plus (fact (minus l k)) X--) (fact (S (minus l k)))) (rewrite-r lzero lzero nat (plus (fact (minus l k)) (times (minus l k) (fact (minus l k)))) (λ (X-- : nat) -> eq lzero nat (plus (fact (minus l k)) (times (minus l k) (fact (minus l k)))) X--) (refl lzero nat (plus (fact (minus l k)) (times (minus l k) (fact (minus l k))))) (fact (S (minus l k))) (rewrite-l lzero lzero nat (times (fact (minus l k)) (minus l k)) (λ (X-- : nat) -> eq lzero nat (fact (S (minus l k))) (plus (fact (minus l k)) X--)) (rewrite-r lzero lzero nat (times (fact (minus l k)) (S (minus l k))) (λ (X-- : nat) -> eq lzero nat (fact (S (minus l k))) X--) (rewrite-l lzero lzero nat (times (S (minus l k)) (fact (minus l k))) (λ (X-- : nat) -> eq lzero nat (fact (S (minus l k))) X--) (factS (minus l k)) (times (fact (minus l k)) (S (minus l k))) (commutative-times (S (minus l k)) (fact (minus l k)))) (plus (fact (minus l k)) (times (fact (minus l k)) (minus l k))) (times-n-Sm (fact (minus l k)) (minus l k))) (times (minus l k) (fact (minus l k))) (commutative-times (fact (minus l k)) (minus l k)))) (times (fact (minus l k)) (minus l k)) (commutative-times (fact (minus l k)) (minus l k))) (times (fact (minus l k)) (S (minus l k))) (times-n-Sm (fact (minus l k)) (minus l k))) (minus (S l) (S k)) (minus-S-S l k)) (minus (S l) k) (minus-Sn-m k l (le-S-S-to-le k l ltl))) n

bc2 : (n : nat) -> (k : nat) -> (X-- : le k n) -> divides (times (fact k) (fact (minus n k))) (fact n)
bc2 = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (k : nat) -> (X-- : le k X-x-365) -> divides (times (fact k) (fact (minus X-x-365 k))) (fact X-x-365)) (λ (k : nat) -> λ (lek0 : le k O) -> eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> divides (times (fact x-1) (fact (minus O x-1))) (fact O)) (divides-n-n (times (fact O) (fact (minus O O)))) k (le-n-O-to-eq k lek0)) (λ (m : nat) -> λ (Hind : (k : nat) -> (X-- : le k m) -> divides (times (fact k) (fact (minus m k))) (fact m)) -> λ (k : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : le X-- (S m)) -> divides (times (fact X--) (fact (minus (S m) X--))) (fact (S m))) (λ (auto : le O (S m)) -> eq-coerc lzero (divides (plus (fact m) (times m (fact m))) (plus (fact m) (times m (fact m)))) (divides (plus (times (fact m) (S m)) O) (times (fact m) (S m))) (divides-n-n (plus (fact m) (times m (fact m)))) (rewrite-l lzero (lsuc lzero) nat (plus (fact m) (times (fact m) m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (divides (plus (fact m) (times m (fact m))) (plus (fact m) (times m (fact m)))) (divides (plus X-- O) (times (fact m) (S m)))) (rewrite-r lzero (lsuc lzero) nat (times m (fact m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (divides (plus (fact m) (times m (fact m))) (plus (fact m) (times m (fact m)))) (divides (plus (plus (fact m) X--) O) (times (fact m) (S m)))) (rewrite-r lzero (lsuc lzero) nat (plus O (plus (fact m) (times m (fact m)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (divides (plus (fact m) (times m (fact m))) (plus (fact m) (times m (fact m)))) (divides X-- (times (fact m) (S m)))) (rewrite-l lzero (lsuc lzero) nat (plus (fact m) (times m (fact m))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (divides (plus (fact m) (times m (fact m))) (plus (fact m) (times m (fact m)))) (divides X-- (times (fact m) (S m)))) (rewrite-l lzero (lsuc lzero) nat (plus (fact m) (times (fact m) m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (divides (plus (fact m) (times m (fact m))) (plus (fact m) (times m (fact m)))) (divides (plus (fact m) (times m (fact m))) X--)) (rewrite-r lzero (lsuc lzero) nat (times m (fact m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (divides (plus (fact m) (times m (fact m))) (plus (fact m) (times m (fact m)))) (divides (plus (fact m) (times m (fact m))) (plus (fact m) X--))) (refl (lsuc lzero) (Set (lzero)) (divides (plus (fact m) (times m (fact m))) (plus (fact m) (times m (fact m))))) (times (fact m) m) (commutative-times (fact m) m)) (times (fact m) (S m)) (times-n-Sm (fact m) m)) (plus O (plus (fact m) (times m (fact m)))) (plus-O-n (plus (fact m) (times m (fact m))))) (plus (plus (fact m) (times m (fact m))) O) (commutative-plus (plus (fact m) (times m (fact m))) O)) (times (fact m) m) (commutative-times (fact m) m)) (times (fact m) (S m)) (times-n-Sm (fact m) m))) (λ (c : nat) -> λ (lec : le (S c) (S m)) -> match-Or lzero lzero (lt c m) (eq lzero nat c m) lzero (λ (X-- : Or lzero lzero (lt c m) (eq lzero nat c m)) -> divides (times (times (fact c) (S c)) (fact (minus m c))) (times (fact m) (S m))) (λ (ltcm : lt c m) -> eq-ind-r lzero lzero nat (S c) (λ (x : nat) -> λ (X-- : eq lzero nat x (S c)) -> (X--1 : divides (times (fact (minus m (S c))) (fact x)) (fact m)) -> divides (times (times (fact c) (S c)) (fact (minus m c))) (times (fact m) (S m))) (λ (Hmc : divides (times (fact (minus m (S c))) (fact (S c))) (fact m)) -> eq-ind-r lzero lzero nat (plus (minus m c) c) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (minus m c) c)) -> divides (times (times (fact c) (S c)) (fact (minus m c))) (times (fact m) (S x))) (eq-ind-r lzero lzero nat (plus c (minus m c)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus c (minus m c))) -> divides (times (times (fact c) (S c)) (fact (minus m c))) (times (fact m) (S x))) (eq-ind-r lzero lzero nat (plus (times (fact m) (S c)) (times (fact m) (minus m c))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (fact m) (S c)) (times (fact m) (minus m c)))) -> divides (times (times (fact c) (S c)) (fact (minus m c))) x) (divides-plus (times (times (fact c) (S c)) (fact (minus m c))) (times (fact m) (S c)) (times (fact m) (minus m c)) (eq-ind-r lzero lzero nat (times (fact c) (times (S c) (fact (minus m c)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (fact c) (times (S c) (fact (minus m c))))) -> divides x (times (fact m) (S c))) (eq-ind-r lzero lzero nat (times (fact (minus m c)) (S c)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (fact (minus m c)) (S c))) -> divides (times (fact c) x) (times (fact m) (S c))) (eq-ind lzero lzero nat (times (times (fact c) (fact (minus m c))) (S c)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (fact c) (fact (minus m c))) (S c)) x-1) -> divides x-1 (times (fact m) (S c))) (divides-times (times (fact c) (fact (minus m c))) (S c) (fact m) (S c) (Hind c (le-S-S-to-le c m lec)) (divides-n-n (S c))) (times (fact c) (times (fact (minus m c)) (S c))) (associative-times (fact c) (fact (minus m c)) (S c))) (times (S c) (fact (minus m c))) (commutative-times (S c) (fact (minus m c)))) (times (times (fact c) (S c)) (fact (minus m c))) (associative-times (fact c) (S c) (fact (minus m c)))) (eq-ind lzero lzero nat (times (fact (minus m (S c))) (minus m c)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (fact (minus m (S c))) (minus m c)) x-1) -> divides (times (times (fact c) (S c)) x-1) (times (fact m) (minus m c))) (eq-ind lzero lzero nat (times (times (times (fact c) (S c)) (fact (minus m (S c)))) (minus m c)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (times (fact c) (S c)) (fact (minus m (S c)))) (minus m c)) x-1) -> divides x-1 (times (fact m) (minus m c))) (divides-times (times (times (fact c) (S c)) (fact (minus m (S c)))) (minus m c) (fact m) (minus m c) (eq-ind-r lzero lzero nat (times (fact (minus m (S c))) (times (fact c) (S c))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (fact (minus m (S c))) (times (fact c) (S c)))) -> divides x (fact m)) Hmc (times (times (fact c) (S c)) (fact (minus m (S c)))) (commutative-times (times (fact c) (S c)) (fact (minus m (S c))))) (divides-n-n (minus m c))) (times (times (fact c) (S c)) (times (fact (minus m (S c))) (minus m c))) (associative-times (times (fact c) (S c)) (fact (minus m (S c))) (minus m c))) (fact (minus m c)) (fact-minus m c ltcm))) (times (fact m) (plus (S c) (minus m c))) (distributive-times-plus (fact m) (S c) (minus m c))) (plus (minus m c) c) (commutative-plus (minus m c) c)) m (plus-minus-m-m m c (le-S-S-to-le c m lec))) (minus m (minus m (S c))) (plus-to-minus m (minus m (S c)) (S c) (plus-minus-m-m m (S c) ltcm)) (Hind (minus m (S c)) (le-plus-to-minus m (S c) m (le-plus-n-r (S c) m)))) (λ (eqcm : eq lzero nat c m) -> eq-ind-r lzero lzero nat m (λ (x : nat) -> λ (X-- : eq lzero nat x m) -> divides (times (times (fact x) (S x)) (fact (minus m x))) (times (fact m) (S m))) (eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> divides (times (times (fact m) (S m)) (fact x-1)) (times (fact m) (S m))) (eq-ind lzero lzero nat (times (fact m) (S m)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (fact m) (S m)) x-1) -> divides x-1 (times (fact m) (S m))) (divides-n-n (times (fact m) (S m))) (times (times (fact m) (S m)) (S O)) (times-n-1 (times (fact m) (S m)))) (minus m m) (minus-n-n m)) c eqcm) (le-to-or-lt-eq c m (le-S-S-to-le c m lec))) k) n

bc1 : (n : nat) -> (k : nat) -> (X-- : lt k n) -> eq lzero nat (bc (S n) (S k)) (plus (bc n k) (bc n (S k)))
bc1 = λ (n : nat) -> λ (k : nat) -> λ (ltkn : lt k n) -> eq-ind-r lzero lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k)))))) -> eq lzero nat x (plus (bc n k) (bc n (S k)))) (eq-ind-r lzero lzero nat (div (fact n) (times (fact k) (fact (minus n k)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (fact n) (times (fact k) (fact (minus n k))))) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (plus x (bc n (S k)))) (eq-ind-r lzero lzero nat (div (fact n) (times (fact (S k)) (fact (minus n (S k))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (fact n) (times (fact (S k)) (fact (minus n (S k)))))) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (plus (div (fact n) (times (fact k) (fact (minus n k)))) x)) (eq-ind-r lzero lzero nat (div (times (fact n) (S k)) (times (times (fact k) (fact (minus n k))) (S k))) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (times (fact n) (S k)) (times (times (fact k) (fact (minus n k))) (S k)))) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (plus x (div (fact n) (times (fact (S k)) (fact (minus n (S k))))))) (eq-ind-r lzero lzero nat (times (fact k) (times (fact (minus n k)) (S k))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (fact k) (times (fact (minus n k)) (S k)))) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (plus (div (times (fact n) (S k)) x) (div (fact n) (times (fact (S k)) (fact (minus n (S k))))))) (eq-ind-r lzero lzero nat (times (S k) (fact (minus n k))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S k) (fact (minus n k)))) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (plus (div (times (fact n) (S k)) (times (fact k) x)) (div (fact n) (times (fact (S k)) (fact (minus n (S k))))))) (eq-ind lzero lzero nat (times (times (fact k) (S k)) (fact (minus n k))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (fact k) (S k)) (fact (minus n k))) x-1) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (plus (div (times (fact n) (S k)) x-1) (div (fact n) (times (fact (S k)) (fact (minus n (S k))))))) (eq-ind-r lzero lzero nat (div (times (fact n) (minus n k)) (times (times (fact (S k)) (fact (minus n (S k)))) (minus n k))) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (times (fact n) (minus n k)) (times (times (fact (S k)) (fact (minus n (S k)))) (minus n k)))) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (plus (div (times (fact n) (S k)) (times (times (fact k) (S k)) (fact (minus n k)))) x)) (eq-ind-r lzero lzero nat (times (fact (S k)) (times (fact (minus n (S k))) (minus n k))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (fact (S k)) (times (fact (minus n (S k))) (minus n k)))) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (plus (div (times (fact n) (S k)) (times (times (fact k) (S k)) (fact (minus n k)))) (div (times (fact n) (minus n k)) x))) (eq-ind-r lzero lzero nat (fact (minus n k)) (λ (x : nat) -> λ (X-- : eq lzero nat x (fact (minus n k))) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (plus (div (times (fact n) (S k)) (times (times (fact k) (S k)) (fact (minus n k)))) (div (times (fact n) (minus n k)) (times (fact (S k)) x)))) (eq-ind lzero lzero nat (div (plus (times (fact n) (S k)) (times (fact n) (minus n k))) (times (times (fact k) (S k)) (fact (minus n k)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (div (plus (times (fact n) (S k)) (times (fact n) (minus n k))) (times (times (fact k) (S k)) (fact (minus n k)))) x-1) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) x-1) (eq-ind lzero lzero nat (times (fact n) (plus (S k) (minus n k))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (fact n) (plus (S k) (minus n k))) x-1) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (div x-1 (times (times (fact k) (S k)) (fact (minus n k))))) (eq-ind-r lzero lzero nat (plus (minus n k) (S k)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (minus n k) (S k))) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (div (times (fact n) x) (times (times (fact k) (S k)) (fact (minus n k))))) (eq-ind lzero lzero nat (S (plus (minus n k) k)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (plus (minus n k) k)) x-1) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (div (times (fact n) x-1) (times (times (fact k) (S k)) (fact (minus n k))))) (eq-ind lzero lzero nat n (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat n x-1) -> eq lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k))))) (div (times (fact n) (S x-1)) (times (times (fact k) (S k)) (fact (minus n k))))) (refl lzero nat (div (fact (S n)) (times (fact (S k)) (fact (minus (S n) (S k)))))) (plus (minus n k) k) (plus-minus-m-m n k (lt-to-le k n ltkn))) (plus (minus n k) (S k)) (plus-n-Sm (minus n k) k)) (plus (S k) (minus n k)) (commutative-plus (S k) (minus n k))) (plus (times (fact n) (S k)) (times (fact n) (minus n k))) (distributive-times-plus (fact n) (S k) (minus n k))) (plus (div (times (fact n) (S k)) (times (times (fact k) (S k)) (fact (minus n k)))) (div (times (fact n) (minus n k)) (times (times (fact k) (S k)) (fact (minus n k))))) (plus-div (times (fact n) (S k)) (times (fact n) (minus n k)) (times (times (fact k) (S k)) (fact (minus n k))) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> lt x (times (times (fact k) (S k)) (fact (minus n k)))) (lt-times O (times (fact k) (S k)) O (fact (minus n k)) (le-1-fact (S k)) (le-1-fact (minus n k))) O (times-n-O O)) (eq-ind-r lzero lzero nat (times (fact k) (times (S k) (fact (minus n k)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (fact k) (times (S k) (fact (minus n k))))) -> divides x (times (fact n) (S k))) (eq-ind-r lzero lzero nat (times (fact (minus n k)) (S k)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (fact (minus n k)) (S k))) -> divides (times (fact k) x) (times (fact n) (S k))) (eq-ind lzero lzero nat (times (times (fact k) (fact (minus n k))) (S k)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (fact k) (fact (minus n k))) (S k)) x-1) -> divides x-1 (times (fact n) (S k))) (divides-times (times (fact k) (fact (minus n k))) (S k) (fact n) (S k) (bc2 n k (lt-to-le k n ltkn)) (divides-n-n (S k))) (times (fact k) (times (fact (minus n k)) (S k))) (associative-times (fact k) (fact (minus n k)) (S k))) (times (S k) (fact (minus n k))) (commutative-times (S k) (fact (minus n k)))) (times (times (fact k) (S k)) (fact (minus n k))) (associative-times (fact k) (S k) (fact (minus n k)))) (eq-ind lzero lzero nat (times (fact (minus n (S k))) (minus n k)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (fact (minus n (S k))) (minus n k)) x-1) -> divides (times (times (fact k) (S k)) x-1) (times (fact n) (minus n k))) (eq-ind lzero lzero nat (times (times (times (fact k) (S k)) (fact (minus n (S k)))) (minus n k)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (times (fact k) (S k)) (fact (minus n (S k)))) (minus n k)) x-1) -> divides x-1 (times (fact n) (minus n k))) (divides-times (times (times (fact k) (S k)) (fact (minus n (S k)))) (minus n k) (fact n) (minus n k) (bc2 n (S k) ltkn) (divides-n-n (minus n k))) (times (times (fact k) (S k)) (times (fact (minus n (S k))) (minus n k))) (associative-times (times (fact k) (S k)) (fact (minus n (S k))) (minus n k))) (fact (minus n k)) (fact-minus n k ltkn)))) (times (fact (minus n (S k))) (minus n k)) (fact-minus n k ltkn)) (times (times (fact (S k)) (fact (minus n (S k)))) (minus n k)) (associative-times (fact (S k)) (fact (minus n (S k))) (minus n k))) (div (fact n) (times (fact (S k)) (fact (minus n (S k))))) (div-times-times (fact n) (times (fact (S k)) (fact (minus n (S k)))) (minus n k) (le-plus-to-le-r k (S O) (minus n k) (eq-ind lzero lzero nat n (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat n x-1) -> le (plus (S O) k) x-1) ltkn (plus (minus n k) k) (plus-minus-m-m n k (lt-to-le k n ltkn)))) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> lt x (times (fact (S k)) (fact (minus n (S k))))) (lt-times O (fact (S k)) O (fact (minus n (S k))) (le-1-fact (S k)) (le-1-fact (minus n (S k)))) O (times-n-O O)))) (times (fact k) (times (S k) (fact (minus n k)))) (associative-times (fact k) (S k) (fact (minus n k)))) (times (fact (minus n k)) (S k)) (commutative-times (fact (minus n k)) (S k))) (times (times (fact k) (fact (minus n k))) (S k)) (associative-times (fact k) (fact (minus n k)) (S k))) (div (fact n) (times (fact k) (fact (minus n k)))) (div-times-times (fact n) (times (fact k) (fact (minus n k))) (S k) (lt-O-S k) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> lt x (times (fact k) (fact (minus n k)))) (lt-times O (fact k) O (fact (minus n k)) (le-1-fact k) (le-1-fact (minus n k))) O (times-n-O O)))) (bc n (S k)) (bceq n (S k))) (bc n k) (bceq n k)) (bc (S n) (S k)) (bceq (S n) (S k))

lt-O-bc : (n : nat) -> (m : nat) -> (X-- : le m n) -> lt O (bc n m)
lt-O-bc = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (m : nat) -> (X-- : le m X-x-365) -> lt O (bc X-x-365 m)) (λ (m : nat) -> λ (lemO : le m O) -> le-n-O-elim lzero m lemO (λ (X-- : nat) -> lt O (bc O X--)) (lt-O-S (div-aux O (minus (fact O) (S (plus O (times O (fact (minus O O)))))) (plus O (times O (fact (minus O O))))))) (λ (n0 : nat) -> λ (Hind : (m : nat) -> (X-- : le m n0) -> lt O (bc n0 m)) -> λ (m : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : le X-- (S n0)) -> lt O (bc (S n0) X--)) (λ (auto : le O (S n0)) -> eq-coerc lzero (lt O (S O)) (lt O (bc (S n0) O)) (lt-O-S O) (rewrite-l lzero (lsuc lzero) nat (bc (S n0) O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O X--) (lt O (bc (S n0) O))) (refl (lsuc lzero) (Set (lzero)) (lt O (bc (S n0) O))) (S O) (bc-n-O (S n0)))) (λ (m0 : nat) -> λ (lemn : le (S m0) (S n0)) -> match-Or lzero lzero (lt m0 n0) (eq lzero nat m0 n0) lzero (λ (X-- : Or lzero lzero (lt m0 n0) (eq lzero nat m0 n0)) -> lt O (bc (S n0) (S m0))) (λ (ltmn : lt m0 n0) -> eq-ind-r lzero lzero nat (plus (bc n0 m0) (bc n0 (S m0))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (bc n0 m0) (bc n0 (S m0)))) -> lt O x) (eq-ind-r lzero lzero nat (plus O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus O O)) -> lt x (plus (bc n0 m0) (bc n0 (S m0)))) (lt-plus O (bc n0 m0) O (bc n0 (S m0)) (Hind m0 (eq-coerc lzero (le (pred (S m0)) (pred (S n0))) (le m0 n0) (monotonic-pred (S m0) (S n0) lemn) (rewrite-l lzero (lsuc lzero) nat m0 (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (pred (S n0))) (le m0 n0)) (rewrite-l lzero (lsuc lzero) nat n0 (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m0 X--) (le m0 n0)) (refl (lsuc lzero) (Set (lzero)) (le m0 n0)) (pred (S n0)) (pred-Sn n0)) (pred (S m0)) (pred-Sn m0)))) (Hind (S m0) ltmn)) O (plus-O-n O)) (bc (S n0) (S m0)) (bc1 n0 m0 ltmn)) (λ (auto : eq lzero nat m0 n0) -> eq-coerc lzero (lt O (S O)) (lt O (bc (S n0) (S m0))) (lt-O-S O) (rewrite-r lzero (lsuc lzero) nat n0 (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O (bc (S n0) (S X--)))) (rewrite-l lzero (lsuc lzero) nat (bc (S n0) (S n0)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O X--) (lt O (bc (S n0) (S n0)))) (refl (lsuc lzero) (Set (lzero)) (lt O (bc (S n0) (S n0)))) (S O) (bc-n-n (S n0))) m0 auto)) (le-to-or-lt-eq m0 n0 (le-S-S-to-le m0 n0 lemn))) m) n

binomial-law : (a : nat) -> (b : nat) -> (n : nat) -> eq lzero nat (exp (plus a b) n) (bigop (S n) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n k) (exp a (minus n k))) (exp b k)))
binomial-law = λ (a : nat) -> λ (b : nat) -> λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat (exp (plus a b) X-x-365) (bigop (S X-x-365) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc X-x-365 k) (exp a (minus X-x-365 k))) (exp b k)))) (refl lzero nat (exp (plus a b) O)) (λ (n0 : nat) -> λ (Hind : eq lzero nat (exp (plus a b) n0) (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k)))) -> eq-ind-r lzero lzero nat (times (plus a b) (exp (plus a b) n0)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (plus a b) (exp (plus a b) n0))) -> eq lzero nat x (bigop (S (S n0)) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc (S n0) k) (exp a (minus (S n0) k))) (exp b k)))) (eq-ind-r lzero lzero nat (plus (times (times (bc (S n0) (S n0)) (exp a (minus (S n0) (S n0)))) (exp b (S n0))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (times (bc (S n0) (S n0)) (exp a (minus (S n0) (S n0)))) (exp b (S n0))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))))) -> eq lzero nat (times (plus a b) (exp (plus a b) n0)) x) (eq-ind-r lzero lzero nat (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k)))) -> eq lzero nat (times (plus a b) x) (plus (times (times (bc (S n0) (S n0)) (exp a (minus (S n0) (S n0)))) (exp b (S n0))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))))) (eq-ind-r lzero lzero nat (plus (times a (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k)))) (times b (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times a (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k)))) (times b (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k)))))) -> eq lzero nat x (plus (times (times (bc (S n0) (S n0)) (exp a (minus (S n0) (S n0)))) (exp b (S n0))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))))) (eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> eq lzero nat (plus (times a (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k)))) (times b (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k))))) (plus (times (times (bc (S n0) (S n0)) (exp a x-1)) (exp b (S n0))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))))) (eq-ind-r lzero lzero nat (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O (sum lzero nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus))) (λ (i : nat) -> prod lzero nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus) a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O (sum lzero nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus))) (λ (i : nat) -> prod lzero nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus) a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) -> eq lzero nat (plus x (times b (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k))))) (plus (times (times (bc (S n0) (S n0)) (exp a O)) (exp b (S n0))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))))) (eq-ind-r lzero lzero nat (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O (sum lzero nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus))) (λ (i : nat) -> prod lzero nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus) b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O (sum lzero nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus))) (λ (i : nat) -> prod lzero nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus) b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) -> eq lzero nat (plus (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) x) (plus (times (times (bc (S n0) (S n0)) (exp a O)) (exp b (S n0))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))))) (eq-ind-r lzero lzero nat (aop--o--op lzero nat O plusAC (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (aop--o--op lzero nat O plusAC (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))))) -> eq lzero nat (plus (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) x) (plus (times (times (bc (S n0) (S n0)) (exp a O)) (exp b (S n0))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))))) (eq-ind lzero lzero nat (plus (plus (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0)))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (plus (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0)))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) x-1) -> eq lzero nat x-1 (plus (times (times (bc (S n0) (S n0)) (exp a O)) (exp b (S n0))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))))) (eq-ind lzero lzero nat (plus (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) x-1) -> eq lzero nat (plus x-1 (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (plus (times (times (bc (S n0) (S n0)) (exp a O)) (exp b (S n0))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))))) (eq-ind-r lzero lzero nat (plus (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (plus (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (plus (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))))) -> eq lzero nat x (plus (times (times (bc (S n0) (S n0)) (exp a O)) (exp b (S n0))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))))) (eq-f2 lzero lzero lzero nat nat nat plus (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (times (times (bc (S n0) (S n0)) (exp a O)) (exp b (S n0))) (plus (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))) (eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> eq lzero nat (times b (times (times (bc n0 n0) (exp a x-1)) (exp b n0))) (times (times (bc (S n0) (S n0)) (exp a O)) (exp b (S n0)))) (eq-ind-r lzero lzero nat (S O) (λ (x : nat) -> λ (X-- : eq lzero nat x (S O)) -> eq lzero nat (times b (times (times x (exp a O)) (exp b n0))) (times (times (bc (S n0) (S n0)) (exp a O)) (exp b (S n0)))) (eq-ind-r lzero lzero nat (S O) (λ (x : nat) -> λ (X-- : eq lzero nat x (S O)) -> eq lzero nat (times b (times (times (S O) (exp a O)) (exp b n0))) (times (times x (exp a O)) (exp b (S n0)))) (rewrite-r lzero lzero nat (plus O (exp b n0)) (λ (X-- : nat) -> eq lzero nat (times b X--) (plus (times (exp b n0) b) O)) (rewrite-l lzero lzero nat (exp b n0) (λ (X-- : nat) -> eq lzero nat (times b X--) (plus (times (exp b n0) b) O)) (rewrite-r lzero lzero nat (times b (exp b n0)) (λ (X-- : nat) -> eq lzero nat (times b (exp b n0)) (plus X-- O)) (rewrite-r lzero lzero nat (plus O (times b (exp b n0))) (λ (X-- : nat) -> eq lzero nat (times b (exp b n0)) X--) (rewrite-l lzero lzero nat (times b (exp b n0)) (λ (X-- : nat) -> eq lzero nat (times b (exp b n0)) X--) (refl lzero nat (times b (exp b n0))) (plus O (times b (exp b n0))) (plus-O-n (times b (exp b n0)))) (plus (times b (exp b n0)) O) (commutative-plus (times b (exp b n0)) O)) (times (exp b n0) b) (commutative-times (exp b n0) b)) (plus O (exp b n0)) (plus-O-n (exp b n0))) (plus (exp b n0) O) (commutative-plus (exp b n0) O)) (bc (S n0) (S n0)) (bc-n-n (S n0))) (bc n0 n0) (bc-n-n n0)) (minus n0 n0) (minus-n-n n0)) (eq-ind-r lzero lzero nat (op lzero nat O plusA (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (op lzero nat O plusA (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O))))) -> eq lzero nat (plus x (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i)))) (eq-ind-r lzero lzero nat (plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (plus (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (plus (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))))) -> eq lzero nat x (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i)))) (eq-ind-r lzero lzero nat (plus (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O))))) -> eq lzero nat (plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) x) (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i)))) (eq-ind lzero lzero nat (plus (plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O)))) x-1) -> eq lzero nat x-1 (bigop (S n0) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i)))) (eq-ind-r lzero lzero nat (op lzero nat O plusA (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i)))) (exp b (S i)))) (times (times (bc (S n0) O) (exp a (minus (S n0) O))) (exp b O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (op lzero nat O plusA (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i)))) (exp b (S i)))) (times (times (bc (S n0) O) (exp a (minus (S n0) O))) (exp b O)))) -> eq lzero nat (plus (plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O)))) x) (eq-f2 lzero lzero lzero nat nat nat plus (plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i)))) (exp b (S i)))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O))) (times (times (bc (S n0) O) (exp a (minus (S n0) O))) (exp b O)) (eq-ind-r lzero lzero nat (aop--o--op lzero nat O plusAC (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (aop--o--op lzero nat O plusAC (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))))) -> eq lzero nat x (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i)))) (exp b (S i))))) (eq-ind-r lzero lzero nat (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> aop--o--op lzero nat O plusAC (times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i)))) (times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> aop--o--op lzero nat O plusAC (times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i)))) (times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))))) -> eq lzero nat x (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i)))) (exp b (S i))))) (same-bigop n0 (λ (X-- : nat) -> true) (λ (X-- : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (X-- : nat) -> aop--o--op lzero nat O plusAC (times a (times (times (bc n0 (S X--)) (exp a (minus n0 (S X--)))) (exp b (S X--)))) (times b (times (times (bc n0 X--) (exp a (minus n0 X--))) (exp b X--)))) (λ (X-- : nat) -> times (times (bc (S n0) (S X--)) (exp a (minus (S n0) (S X--)))) (exp b (S X--))) (λ (i : nat) -> λ (auto : lt i n0) -> refl lzero bool true) (λ (i : nat) -> λ (ltin : lt i n0) -> λ (X-- : eq lzero bool true true) -> eq-ind lzero lzero nat (times (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (exp b (S i))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (exp b (S i))) x-1) -> eq lzero nat (aop--o--op lzero nat O plusAC x-1 (times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (times (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i)))) (exp b (S i)))) (eq-ind-r lzero lzero nat (times (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)) b) (λ (x : nat) -> λ (X-0 : eq lzero nat x (times (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)) b)) -> eq lzero nat (aop--o--op lzero nat O plusAC (times (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (exp b (S i))) x) (times (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i)))) (exp b (S i)))) (eq-ind-r lzero lzero nat (times (times (bc n0 i) (exp a (minus n0 i))) (times (exp b i) b)) (λ (x : nat) -> λ (X-0 : eq lzero nat x (times (times (bc n0 i) (exp a (minus n0 i))) (times (exp b i) b))) -> eq lzero nat (aop--o--op lzero nat O plusAC (times (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (exp b (S i))) x) (times (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i)))) (exp b (S i)))) (eq-ind lzero lzero nat (plus (times (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (exp b (S i))) (times (times (bc n0 i) (exp a (minus n0 i))) (times (exp b i) b))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (times (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (exp b (S i))) (times (times (bc n0 i) (exp a (minus n0 i))) (times (exp b i) b))) x-1) -> eq lzero nat x-1 (times (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i)))) (exp b (S i)))) (eq-ind lzero lzero nat (times (plus (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (times (bc n0 i) (exp a (minus n0 i)))) (exp b (S i))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (plus (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (times (bc n0 i) (exp a (minus n0 i)))) (exp b (S i))) x-1) -> eq lzero nat x-1 (times (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i)))) (exp b (S i)))) (eq-f2 lzero lzero lzero nat nat nat times (plus (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (times (bc n0 i) (exp a (minus n0 i)))) (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i)))) (exp b (S i)) (exp b (S i)) (eq-ind lzero lzero nat (times (times a (bc n0 (S i))) (exp a (minus n0 (S i)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times a (bc n0 (S i))) (exp a (minus n0 (S i)))) x-1) -> eq lzero nat (plus x-1 (times (bc n0 i) (exp a (minus n0 i)))) (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i))))) (eq-ind-r lzero lzero nat (times (bc n0 (S i)) a) (λ (x : nat) -> λ (X-0 : eq lzero nat x (times (bc n0 (S i)) a)) -> eq lzero nat (plus (times x (exp a (minus n0 (S i)))) (times (bc n0 i) (exp a (minus n0 i)))) (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i))))) (eq-ind-r lzero lzero nat (times (bc n0 (S i)) (times a (exp a (minus n0 (S i))))) (λ (x : nat) -> λ (X-0 : eq lzero nat x (times (bc n0 (S i)) (times a (exp a (minus n0 (S i)))))) -> eq lzero nat (plus x (times (bc n0 i) (exp a (minus n0 i)))) (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i))))) (eq-ind-r lzero lzero nat (exp a (S (minus n0 (S i)))) (λ (x : nat) -> λ (X-0 : eq lzero nat x (exp a (S (minus n0 (S i))))) -> eq lzero nat (plus (times (bc n0 (S i)) x) (times (bc n0 i) (exp a (minus n0 i)))) (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i))))) (eq-ind lzero lzero nat (minus (S n0) (S i)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (minus (S n0) (S i)) x-1) -> eq lzero nat (plus (times (bc n0 (S i)) (exp a x-1)) (times (bc n0 i) (exp a (minus n0 i)))) (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i))))) (eq-ind lzero lzero nat (times (plus (bc n0 (S i)) (bc n0 i)) (exp a (minus n0 i))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (plus (bc n0 (S i)) (bc n0 i)) (exp a (minus n0 i))) x-1) -> eq lzero nat x-1 (times (bc (S n0) (S i)) (exp a (minus (S n0) (S i))))) (eq-f2 lzero lzero lzero nat nat nat times (plus (bc n0 (S i)) (bc n0 i)) (bc (S n0) (S i)) (exp a (minus n0 i)) (exp a (minus (S n0) (S i))) (sym-eq lzero nat (bc (S n0) (S i)) (plus (bc n0 (S i)) (bc n0 i)) (eq-ind-r lzero lzero nat (plus (bc n0 i) (bc n0 (S i))) (λ (x : nat) -> λ (X-0 : eq lzero nat x (plus (bc n0 i) (bc n0 (S i)))) -> eq lzero nat (bc (S n0) (S i)) x) (bc1 n0 i ltin) (plus (bc n0 (S i)) (bc n0 i)) (commutative-plus (bc n0 (S i)) (bc n0 i)))) (rewrite-r lzero lzero nat (minus n0 i) (λ (X--1 : nat) -> eq lzero nat (exp a (minus n0 i)) (exp a X--1)) (refl lzero nat (exp a (minus n0 i))) (minus (S n0) (S i)) (minus-S-S n0 i))) (plus (times (bc n0 (S i)) (exp a (minus n0 i))) (times (bc n0 i) (exp a (minus n0 i)))) (distributive-times-plus-r (exp a (minus n0 i)) (bc n0 (S i)) (bc n0 i))) (S (minus n0 (S i))) (minus-Sn-m (S i) n0 ltin)) (times a (exp a (minus n0 (S i)))) (commutative-times a (exp a (minus n0 (S i))))) (times (times (bc n0 (S i)) a) (exp a (minus n0 (S i)))) (associative-times (bc n0 (S i)) a (exp a (minus n0 (S i))))) (times a (bc n0 (S i))) (commutative-times a (bc n0 (S i)))) (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (associative-times a (bc n0 (S i)) (exp a (minus n0 (S i))))) (refl lzero nat (exp b (S i)))) (plus (times (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (exp b (S i))) (times (times (bc n0 i) (exp a (minus n0 i))) (exp b (S i)))) (distributive-times-plus-r (exp b (S i)) (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (times (bc n0 i) (exp a (minus n0 i))))) (aop--o--op lzero nat O plusAC (times (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (exp b (S i))) (times (times (bc n0 i) (exp a (minus n0 i))) (times (exp b i) b))) (refl lzero nat (plus (times (times a (times (bc n0 (S i)) (exp a (minus n0 (S i))))) (exp b (S i))) (times (times (bc n0 i) (exp a (minus n0 i))) (times (exp b i) b))))) (times (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)) b) (associative-times (times (bc n0 i) (exp a (minus n0 i))) (exp b i) b)) (times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))) (commutative-times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i)))) (associative-times a (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (aop--o--op lzero nat O plusAC (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (bigop-op n0 (λ (X-- : nat) -> true) nat O plusAC (λ (X-- : nat) -> times a (times (times (bc n0 (S X--)) (exp a (minus n0 (S X--)))) (exp b (S X--)))) (λ (X-- : nat) -> times b (times (times (bc n0 X--) (exp a (minus n0 X--))) (exp b X--))))) (plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (refl lzero nat (plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))))) (eq-ind-r lzero lzero nat (S O) (λ (x : nat) -> λ (X-- : eq lzero nat x (S O)) -> eq lzero nat (times a (times (times x (exp a (minus n0 O))) (exp b O))) (times (times (bc (S n0) O) (exp a (minus (S n0) O))) (exp b O))) (eq-ind-r lzero lzero nat (S O) (λ (x : nat) -> λ (X-- : eq lzero nat x (S O)) -> eq lzero nat (times a (times (times (S O) (exp a (minus n0 O))) (exp b O))) (times (times x (exp a (minus (S n0) O))) (exp b O))) (rewrite-l lzero lzero nat n0 (λ (X-- : nat) -> eq lzero nat (times a (times (plus (exp a X--) O) (S O))) (times (plus (times (exp a n0) a) O) (S O))) (rewrite-r lzero lzero nat (plus O (exp a n0)) (λ (X-- : nat) -> eq lzero nat (times a (times X-- (S O))) (times (plus (times (exp a n0) a) O) (S O))) (rewrite-l lzero lzero nat (exp a n0) (λ (X-- : nat) -> eq lzero nat (times a (times X-- (S O))) (times (plus (times (exp a n0) a) O) (S O))) (rewrite-l lzero lzero nat (plus (exp a n0) (times (exp a n0) O)) (λ (X-- : nat) -> eq lzero nat (times a X--) (times (plus (times (exp a n0) a) O) (S O))) (rewrite-r lzero lzero nat (times O (exp a n0)) (λ (X-- : nat) -> eq lzero nat (times a (plus (exp a n0) X--)) (times (plus (times (exp a n0) a) O) (S O))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (times a (plus (exp a n0) X--)) (times (plus (times (exp a n0) a) O) (S O))) (rewrite-r lzero lzero nat (plus O (exp a n0)) (λ (X-- : nat) -> eq lzero nat (times a X--) (times (plus (times (exp a n0) a) O) (S O))) (rewrite-l lzero lzero nat (exp a n0) (λ (X-- : nat) -> eq lzero nat (times a X--) (times (plus (times (exp a n0) a) O) (S O))) (rewrite-r lzero lzero nat (times a (exp a n0)) (λ (X-- : nat) -> eq lzero nat (times a (exp a n0)) (times (plus X-- O) (S O))) (rewrite-r lzero lzero nat (plus O (times a (exp a n0))) (λ (X-- : nat) -> eq lzero nat (times a (exp a n0)) (times X-- (S O))) (rewrite-l lzero lzero nat (times a (exp a n0)) (λ (X-- : nat) -> eq lzero nat (times a (exp a n0)) (times X-- (S O))) (rewrite-r lzero lzero nat (times a (times (exp a n0) (S O))) (λ (X-- : nat) -> eq lzero nat (times a (exp a n0)) X--) (rewrite-l lzero lzero nat (plus (exp a n0) (times (exp a n0) O)) (λ (X-- : nat) -> eq lzero nat (times a (exp a n0)) (times a X--)) (rewrite-r lzero lzero nat (times O (exp a n0)) (λ (X-- : nat) -> eq lzero nat (times a (exp a n0)) (times a (plus (exp a n0) X--))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (times a (exp a n0)) (times a (plus (exp a n0) X--))) (rewrite-r lzero lzero nat (plus O (exp a n0)) (λ (X-- : nat) -> eq lzero nat (times a (exp a n0)) (times a X--)) (rewrite-l lzero lzero nat (exp a n0) (λ (X-- : nat) -> eq lzero nat (times a (exp a n0)) (times a X--)) (refl lzero nat (times a (exp a n0))) (plus O (exp a n0)) (plus-O-n (exp a n0))) (plus (exp a n0) O) (commutative-plus (exp a n0) O)) (times O (exp a n0)) (times-O-n (exp a n0))) (times (exp a n0) O) (commutative-times (exp a n0) O)) (times (exp a n0) (S O)) (times-n-Sm (exp a n0) O)) (times (times a (exp a n0)) (S O)) (associative-times a (exp a n0) (S O))) (plus O (times a (exp a n0))) (plus-O-n (times a (exp a n0)))) (plus (times a (exp a n0)) O) (commutative-plus (times a (exp a n0)) O)) (times (exp a n0) a) (commutative-times (exp a n0) a)) (plus O (exp a n0)) (plus-O-n (exp a n0))) (plus (exp a n0) O) (commutative-plus (exp a n0) O)) (times O (exp a n0)) (times-O-n (exp a n0))) (times (exp a n0) O) (commutative-times (exp a n0) O)) (times (exp a n0) (S O)) (times-n-Sm (exp a n0) O)) (plus O (exp a n0)) (plus-O-n (exp a n0))) (plus (exp a n0) O) (commutative-plus (exp a n0) O)) (minus n0 O) (minus-n-O n0)) (bc (S n0) O) (bc-n-O (S n0))) (bc n0 O) (bc-n-O n0))) (bigop (S n0) (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))) (bigop-0 n0 nat O plusA (λ (X-- : nat) -> times (times (bc (S n0) X--) (exp a (minus (S n0) X--))) (exp b X--)))) (plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (plus (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O))))) (associative-plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O))))) (plus (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (commutative-plus (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))))) (plus (plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O)))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (associative-plus (bigop n0 (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 (S i)) (exp a (minus n0 (S i)))) (exp b (S i))))) (times a (times (times (bc n0 O) (exp a (minus n0 O))) (exp b O))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))))) (bigop (S n0) (λ (i : nat) -> true) nat O (op lzero nat O plusA) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (bigop-0 n0 nat O plusA (λ (X-- : nat) -> times a (times (times (bc n0 X--) (exp a (minus n0 X--))) (exp b X--)))))) (plus (plus (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i))))) (associative-plus (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))))) (plus (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0)))) (commutative-plus (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))))) (plus (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (plus (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))))) (associative-plus (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times a (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (times b (times (times (bc n0 n0) (exp a (minus n0 n0))) (exp b n0))) (bigop n0 (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))))) (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times b (times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (bigop-Strue n0 (λ (X-- : nat) -> true) nat O (aop--o--op lzero nat O plusAC) (λ (X-- : nat) -> times b (times (times (bc n0 X--) (exp a (minus n0 X--))) (exp b X--))) (refl lzero bool true))) (times b (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O (sum lzero nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus))) (λ (i : nat) -> times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (bigop-distr (S n0) (λ (X-- : nat) -> true) nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus) (λ (X-- : nat) -> times (times (bc n0 X--) (exp a (minus n0 X--))) (exp b X--)) b)) (times a (bigop (S n0) (λ (i : nat) -> true) nat O (aop--o--op lzero nat O (sum lzero nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus))) (λ (i : nat) -> times (times (bc n0 i) (exp a (minus n0 i))) (exp b i)))) (bigop-distr (S n0) (λ (X-- : nat) -> true) nat O (mk-Dop lzero nat O plusAC times (λ (n00 : nat) -> sym-eq lzero nat O (times n00 O) (times-n-O n00)) distributive-times-plus) (λ (X-- : nat) -> times (times (bc n0 X--) (exp a (minus n0 X--))) (exp b X--)) a)) (minus (S n0) (S n0)) (minus-n-n (S n0))) (times (plus a b) (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k)))) (distributive-times-plus-r (bigop (S n0) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n0 k) (exp a (minus n0 k))) (exp b k))) a b)) (exp (plus a b) n0) Hind) (bigop (S (S n0)) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> times (times (bc (S n0) i) (exp a (minus (S n0) i))) (exp b i))) (bigop-Strue (S n0) (λ (X-- : nat) -> true) nat O plus (λ (X-- : nat) -> times (times (bc (S n0) X--) (exp a (minus (S n0) X--))) (exp b X--)) (refl lzero bool true))) (times (exp (plus a b) n0) (plus a b)) (commutative-times (exp (plus a b) n0) (plus a b))) n

exp-S-sigma-p : (a : nat) -> (n : nat) -> eq lzero nat (exp (S a) n) (bigop (S n) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (bc n k) (exp a (minus n k))))
exp-S-sigma-p = λ (a : nat) -> λ (n : nat) -> eq-ind-r lzero lzero nat (plus a (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus a (S O))) -> eq lzero nat (exp x n) (bigop (S n) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (bc n k) (exp a (minus n k))))) (eq-ind-r lzero lzero nat (bigop (S n) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n k) (exp a (minus n k))) (exp (S O) k))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc n k) (exp a (minus n k))) (exp (S O) k)))) -> eq lzero nat x (bigop (S n) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (bc n k) (exp a (minus n k))))) (same-bigop (S n) (λ (X-- : nat) -> true) (λ (X-- : nat) -> true) nat O plus (λ (X-- : nat) -> times (times (bc n X--) (exp a (minus n X--))) (exp (S O) X--)) (λ (X-- : nat) -> times (bc n X--) (exp a (minus n X--))) (λ (i : nat) -> λ (auto : lt i (S n)) -> refl lzero bool true) (λ (i : nat) -> λ (auto : lt i (S n)) -> λ (auto' : eq lzero bool true true) -> rewrite-l lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (times (times (bc n i) (exp a (minus n i))) X--) (times (bc n i) (exp a (minus n i)))) (rewrite-r lzero lzero nat (times (bc n i) (times (exp a (minus n i)) (S O))) (λ (X-- : nat) -> eq lzero nat X-- (times (bc n i) (exp a (minus n i)))) (rewrite-l lzero lzero nat (plus (exp a (minus n i)) (times (exp a (minus n i)) O)) (λ (X-- : nat) -> eq lzero nat (times (bc n i) X--) (times (bc n i) (exp a (minus n i)))) (rewrite-r lzero lzero nat (times O (exp a (minus n i))) (λ (X-- : nat) -> eq lzero nat (times (bc n i) (plus (exp a (minus n i)) X--)) (times (bc n i) (exp a (minus n i)))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (times (bc n i) (plus (exp a (minus n i)) X--)) (times (bc n i) (exp a (minus n i)))) (rewrite-r lzero lzero nat (plus O (exp a (minus n i))) (λ (X-- : nat) -> eq lzero nat (times (bc n i) X--) (times (bc n i) (exp a (minus n i)))) (rewrite-l lzero lzero nat (exp a (minus n i)) (λ (X-- : nat) -> eq lzero nat (times (bc n i) X--) (times (bc n i) (exp a (minus n i)))) (refl lzero nat (times (bc n i) (exp a (minus n i)))) (plus O (exp a (minus n i))) (plus-O-n (exp a (minus n i)))) (plus (exp a (minus n i)) O) (commutative-plus (exp a (minus n i)) O)) (times O (exp a (minus n i))) (times-O-n (exp a (minus n i)))) (times (exp a (minus n i)) O) (commutative-times (exp a (minus n i)) O)) (times (exp a (minus n i)) (S O)) (times-n-Sm (exp a (minus n i)) O)) (times (times (bc n i) (exp a (minus n i))) (S O)) (associative-times (bc n i) (exp a (minus n i)) (S O))) (exp (S O) i) (exp-1-n i))) (exp (plus a (S O)) n) (binomial-law a (S O) n)) (S a) (rewrite-r lzero lzero nat (plus a (S O)) (λ (X-- : nat) -> eq lzero nat X-- (plus a (S O))) (refl lzero nat (plus a (S O))) (S a) (rewrite-r lzero lzero nat (plus a O) (λ (X-- : nat) -> eq lzero nat (S X--) (plus a (S O))) (plus-n-Sm a O) a (plus-n-O a)))

eqb-sym : (a : nat) -> (b : nat) -> eq lzero bool (eqb a b) (eqb b a)
eqb-sym = λ (a : nat) -> λ (b : nat) -> match-Or lzero lzero (eq lzero bool (eqb a b) true) (eq lzero bool (eqb a b) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (eqb a b) true) (eq lzero bool (eqb a b) false)) -> eq lzero bool (eqb a b) (eqb b a)) (λ (Hab : eq lzero bool (eqb a b) true) -> eq-ind-r lzero lzero nat b (λ (x : nat) -> λ (X-- : eq lzero nat x b) -> eq lzero bool (eqb x b) (eqb b x)) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- (eqb b b)) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool true X--) (refl lzero bool true) (eqb b b) (eqb-n-n b)) (eqb b b) (eqb-n-n b)) a (eqb-true-to-eq a b Hab)) (λ (Hab : eq lzero bool (eqb a b) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool x (eqb b a)) (sym-eq lzero bool (eqb b a) false (not-eq-to-eqb-false b a (not-to-not lzero (eq lzero nat b a) (eq lzero nat a b) (λ (auto : eq lzero nat b a) -> rewrite-r lzero lzero nat a (λ (X-- : nat) -> eq lzero nat a X--) (refl lzero nat a) b auto) (eqb-false-to-not-eq a b Hab)))) (eqb a b) Hab) (true-or-false (eqb a b))

M : (X-m : nat) -> nat
M = λ (m : nat) -> bc (S (times (S (S O)) m)) m

Mdef : (m : nat) -> eq lzero nat (M m) (bc (S (times (S (S O)) m)) m)
Mdef = λ (m : nat) -> refl lzero nat (M m)

let-clause-1692 : (m : nat) -> (posm : lt O m) -> (a : nat) -> (x358 : nat) -> (x359 : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC x358 (times x358 x359)) (times x358 (S x359))
let-clause-1692 = λ (m : nat) -> λ (posm : lt O m) -> λ (a : nat) -> λ (x358 : nat) -> λ (x359 : nat) -> rewrite-l lzero lzero nat (plus x358 (times x358 x359)) (λ (X-- : nat) -> eq lzero nat X-- (times x358 (S x359))) (times-n-Sm x358 x359) (aop--o--op lzero nat O plusAC x358 (times x358 x359)) (refl lzero nat (plus x358 (times x358 x359)))

let-clause-1704 : (m : nat) -> (posm : lt O m) -> (a : nat) -> (x1029 : nat) -> eq lzero nat x1029 (aop--o--op lzero nat O plusAC x1029 O)
let-clause-1704 = λ (m : nat) -> λ (posm : lt O m) -> λ (a : nat) -> λ (x1029 : nat) -> rewrite-r lzero lzero nat (times x1029 O) (λ (X-- : nat) -> eq lzero nat x1029 (aop--o--op lzero nat O plusAC x1029 X--)) (rewrite-r lzero lzero nat (times x1029 (S O)) (λ (X-- : nat) -> eq lzero nat x1029 X--) (times-n-1 x1029) (aop--o--op lzero nat O plusAC x1029 (times x1029 O)) (let-clause-1692 m posm a x1029 O)) O (times-n-O x1029)

let-clause-16921 : (m : nat) -> (posm : lt O m) -> (a : nat) -> (x358 : nat) -> (x359 : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC x358 (times x358 x359)) (times x358 (S x359))
let-clause-16921 = λ (m : nat) -> λ (posm : lt O m) -> λ (a : nat) -> λ (x358 : nat) -> λ (x359 : nat) -> rewrite-l lzero lzero nat (plus x358 (times x358 x359)) (λ (X-- : nat) -> eq lzero nat X-- (times x358 (S x359))) (times-n-Sm x358 x359) (aop--o--op lzero nat O plusAC x358 (times x358 x359)) (refl lzero nat (plus x358 (times x358 x359)))

let-clause-17041 : (m : nat) -> (posm : lt O m) -> (a : nat) -> (x1029 : nat) -> eq lzero nat x1029 (aop--o--op lzero nat O plusAC x1029 O)
let-clause-17041 = λ (m : nat) -> λ (posm : lt O m) -> λ (a : nat) -> λ (x1029 : nat) -> rewrite-r lzero lzero nat (times x1029 O) (λ (X-- : nat) -> eq lzero nat x1029 (aop--o--op lzero nat O plusAC x1029 X--)) (rewrite-r lzero lzero nat (times x1029 (S O)) (λ (X-- : nat) -> eq lzero nat x1029 X--) (times-n-1 x1029) (aop--o--op lzero nat O plusAC x1029 (times x1029 O)) (let-clause-16921 m posm a x1029 O)) O (times-n-O x1029)

lt-M : (m : nat) -> (X-- : lt O m) -> lt (M m) (exp (S (S O)) (times (S (S O)) m))
lt-M = λ (m : nat) -> λ (posm : lt O m) -> lt-times-n-to-lt-l (S (S O)) (M m) (exp (S (S O)) (times (S (S O)) m)) (eq-ind lzero lzero nat (exp (S (S O)) (S (times (S (S O)) m))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp (S (S O)) (S (times (S (S O)) m))) x-1) -> lt (times (M m) (S (S O))) x-1) (eq-ind-r lzero lzero nat (plus (S O) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S O) (S O))) -> lt (times (M m) (S (S O))) (exp x (S (times (S (S O)) m)))) (eq-ind-r lzero lzero nat (bigop (S (S (times (S (S O)) m))) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc (S (times (S (S O)) m)) k) (exp (S O) (minus (S (times (S (S O)) m)) k))) (exp (S O) k))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (S (times (S (S O)) m))) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc (S (times (S (S O)) m)) k) (exp (S O) (minus (S (times (S (S O)) m)) k))) (exp (S O) k)))) -> lt (times (M m) (S (S O))) x) (le-to-lt-to-lt (times (M m) (S (S O))) (bigop (S (S (times (S (S O)) m))) (λ (k : nat) -> orb (eqb k m) (eqb k (S m))) nat O plus (λ (k : nat) -> times (times (bc (S (times (S (S O)) m)) k) (exp (S O) (minus (S (times (S (S O)) m)) k))) (exp (S O) k))) (bigop (S (S (times (S (S O)) m))) (λ (k : nat) -> true) nat O plus (λ (k : nat) -> times (times (bc (S (times (S (S O)) m)) k) (exp (S O) (minus (S (times (S (S O)) m)) k))) (exp (S O) k))) (eq-ind-r lzero lzero nat (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) m) (exp (S O) (minus (S (times (S (S O)) m)) m))) (exp (S O) m)) (bigop (S (S (times (S (S O)) m))) (λ (x : nat) -> andb (notb (eqb m x)) (orb (eqb x m) (eqb x (S m)))) nat O (aop--o--op lzero nat O plusAC) (λ (x : nat) -> times (times (bc (S (times (S (S O)) m)) x) (exp (S O) (minus (S (times (S (S O)) m)) x))) (exp (S O) x)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) m) (exp (S O) (minus (S (times (S (S O)) m)) m))) (exp (S O) m)) (bigop (S (S (times (S (S O)) m))) (λ (x0 : nat) -> andb (notb (eqb m x0)) (orb (eqb x0 m) (eqb x0 (S m)))) nat O (aop--o--op lzero nat O plusAC) (λ (x0 : nat) -> times (times (bc (S (times (S (S O)) m)) x0) (exp (S O) (minus (S (times (S (S O)) m)) x0))) (exp (S O) x0))))) -> le (times (M m) (S (S O))) x) (eq-ind-r lzero lzero nat (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) (bigop (S (S (times (S (S O)) m))) (λ (x : nat) -> andb (notb (eqb (S m) x)) (andb (notb (eqb m x)) (orb (eqb x m) (eqb x (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (x : nat) -> times (times (bc (S (times (S (S O)) m)) x) (exp (S O) (minus (S (times (S (S O)) m)) x))) (exp (S O) x)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) (bigop (S (S (times (S (S O)) m))) (λ (x0 : nat) -> andb (notb (eqb (S m) x0)) (andb (notb (eqb m x0)) (orb (eqb x0 m) (eqb x0 (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (x0 : nat) -> times (times (bc (S (times (S (S O)) m)) x0) (exp (S O) (minus (S (times (S (S O)) m)) x0))) (exp (S O) x0))))) -> le (times (M m) (S (S O))) (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) m) (exp (S O) (minus (S (times (S (S O)) m)) m))) (exp (S O) m)) x)) (eq-ind lzero lzero nat (bigop O (λ (i : nat) -> andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb i m) (eqb i (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bigop O (λ (i : nat) -> andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb i m) (eqb i (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i))) x-1) -> le (times (M m) (S (S O))) (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) m) (exp (S O) (minus (S (times (S (S O)) m)) m))) (exp (S O) m)) (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) x-1))) (eq-ind lzero lzero nat (plus (times (times (bc (S (times (S (S O)) m)) m) (exp (S O) (minus (S (times (S (S O)) m)) m))) (exp (S O) m)) (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) (bigop O (λ (i : nat) -> andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb i m) (eqb i (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (times (times (bc (S (times (S (S O)) m)) m) (exp (S O) (minus (S (times (S (S O)) m)) m))) (exp (S O) m)) (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) (bigop O (λ (i : nat) -> andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb i m) (eqb i (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i))))) x-1) -> le (times (M m) (S (S O))) x-1) (eq-ind lzero lzero nat (plus (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) (bigop O (λ (i : nat) -> andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb i m) (eqb i (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) (bigop O (λ (i : nat) -> andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb i m) (eqb i (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i)))) x-1) -> le (times (M m) (S (S O))) (plus (times (times (bc (S (times (S (S O)) m)) m) (exp (S O) (minus (S (times (S (S O)) m)) m))) (exp (S O) m)) x-1)) (eq-ind-r lzero lzero nat (times (S (S O)) (M m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) (M m))) -> le x (plus (times (times (bc (S (times (S (S O)) m)) m) (exp (S O) (minus (S (times (S (S O)) m)) m))) (exp (S O) m)) (plus (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) O))) (eq-ind-r lzero lzero nat (plus (M m) (M m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (M m) (M m))) -> le x (plus (times (times (bc (S (times (S (S O)) m)) m) (exp (S O) (minus (S (times (S (S O)) m)) m))) (exp (S O) m)) (plus (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) O))) (eq-ind lzero lzero nat (S O) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S O) x-1) -> le (plus (M m) (M m)) (plus (times (times (bc (S (times (S (S O)) m)) m) x-1) (exp (S O) m)) (plus (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) O))) (eq-ind lzero lzero nat (S O) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S O) x-1) -> le (plus (M m) (M m)) (plus (times (times (bc (S (times (S (S O)) m)) m) (S O)) x-1) (plus (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) O))) (eq-ind lzero lzero nat (S O) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S O) x-1) -> le (plus (M m) (M m)) (plus (times (times (bc (S (times (S (S O)) m)) m) (S O)) (S O)) (plus (times (times (bc (S (times (S (S O)) m)) (S m)) x-1) (exp (S O) (S m))) O))) (eq-ind lzero lzero nat (S O) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S O) x-1) -> le (plus (M m) (M m)) (plus (times (times (bc (S (times (S (S O)) m)) m) (S O)) (S O)) (plus (times (times (bc (S (times (S (S O)) m)) (S m)) (S O)) x-1) O))) (eq-ind lzero lzero nat (times (bc (S (times (S (S O)) m)) m) (S O)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (bc (S (times (S (S O)) m)) m) (S O)) x-1) -> le (plus (M m) (M m)) (plus x-1 (plus (times (times (bc (S (times (S (S O)) m)) (S m)) (S O)) (S O)) O))) (eq-ind lzero lzero nat (bc (S (times (S (S O)) m)) m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bc (S (times (S (S O)) m)) m) x-1) -> le (plus (M m) (M m)) (plus x-1 (plus (times (times (bc (S (times (S (S O)) m)) (S m)) (S O)) (S O)) O))) (eq-ind lzero lzero nat (times (bc (S (times (S (S O)) m)) (S m)) (S O)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (bc (S (times (S (S O)) m)) (S m)) (S O)) x-1) -> le (plus (M m) (M m)) (plus (bc (S (times (S (S O)) m)) m) (plus x-1 O))) (eq-ind lzero lzero nat (bc (S (times (S (S O)) m)) (S m)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bc (S (times (S (S O)) m)) (S m)) x-1) -> le (plus (M m) (M m)) (plus (bc (S (times (S (S O)) m)) m) (plus x-1 O))) (le-plus (M m) (bc (S (times (S (S O)) m)) m) (M m) (plus (bc (S (times (S (S O)) m)) (S m)) O) (le-n (M m)) (eq-ind-r lzero lzero nat (bc (S (times (S (S O)) m)) m) (λ (x : nat) -> λ (X-- : eq lzero nat x (bc (S (times (S (S O)) m)) m)) -> le x (plus (bc (S (times (S (S O)) m)) (S m)) O)) (eq-ind lzero lzero nat (bc (S (times (S (S O)) m)) (S m)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bc (S (times (S (S O)) m)) (S m)) x-1) -> le (bc (S (times (S (S O)) m)) m) x-1) (eq-ind-r lzero lzero nat (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (minus (S (times (S (S O)) m)) m))))) -> le x (bc (S (times (S (S O)) m)) (S m))) (eq-ind-r lzero lzero nat (div (fact (S (times (S (S O)) m))) (times (fact (S m)) (fact (minus (S (times (S (S O)) m)) (S m))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (fact (S (times (S (S O)) m))) (times (fact (S m)) (fact (minus (S (times (S (S O)) m)) (S m)))))) -> le (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) x) (eq-ind-r lzero lzero nat (minus (times (S (S O)) m) m) (λ (x : nat) -> λ (X-- : eq lzero nat x (minus (times (S (S O)) m) m)) -> le (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (div (fact (S (times (S (S O)) m))) (times (fact (S m)) (fact x)))) (eq-ind lzero lzero nat m (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat m x-1) -> le (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (div (fact (S (times (S (S O)) m))) (times (fact (S m)) (fact (minus (plus m x-1) m))))) (eq-ind lzero lzero nat m (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat m x-1) -> le (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (div (fact (S (times (S (S O)) m))) (times (fact (S m)) (fact x-1)))) (eq-ind lzero lzero nat (times (fact m) (fact (S m))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (fact m) (fact (S m))) x-1) -> le (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (div (fact (S (times (S (S O)) m))) x-1)) (eq-ind-r lzero lzero nat (S m) (λ (x : nat) -> λ (X-- : eq lzero nat x (S m)) -> le (div (fact (S (times (S (S O)) m))) (times (fact m) (fact x))) (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (S m))))) (le-n (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (S m))))) (minus (S (times (S (S O)) m)) m) (eq-ind-r lzero lzero nat (plus m m) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus m m)) -> eq lzero nat (minus (S x) m) (S m)) (eq-ind-r lzero lzero nat (plus m (S m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus m (S m))) -> eq lzero nat (minus x m) (S m)) (eq-ind-r lzero lzero nat (plus (S m) m) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S m) m)) -> eq lzero nat (minus x m) (S m)) (eq-ind lzero lzero nat (S m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S m) x-1) -> eq lzero nat x-1 (S m)) (refl lzero nat (S m)) (minus (plus (S m) m) m) (minus-plus-m-m (S m) m)) (plus m (S m)) (commutative-plus m (S m))) (S (plus m m)) (plus-n-Sm m m)) (times (S (S O)) m) (rewrite-r lzero lzero nat (aop--o--op lzero nat O plusAC (S O) (S O)) (λ (X-- : nat) -> eq lzero nat (times X-- m) (plus m m)) (rewrite-r lzero lzero nat (times m (aop--o--op lzero nat O plusAC (S O) (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus m m)) (rewrite-r lzero lzero nat (aop--o--op lzero nat O plusAC (times m (S O)) (times m (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus m m)) (rewrite-l lzero lzero nat (aop--o--op lzero nat O plusAC m (times m O)) (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC X-- (times m (S O))) (plus m m)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC (aop--o--op lzero nat O plusAC m X--) (times m (S O))) (plus m m)) (rewrite-l lzero lzero nat m (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC X-- (times m (S O))) (plus m m)) (rewrite-l lzero lzero nat (aop--o--op lzero nat O plusAC m (times m O)) (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC m X--) (plus m m)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC m (aop--o--op lzero nat O plusAC m X--)) (plus m m)) (rewrite-l lzero lzero nat m (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC m X--) (plus m m)) (rewrite-r lzero lzero nat (aop--o--op lzero nat O plusAC m m) (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC m m) X--) (refl lzero nat (aop--o--op lzero nat O plusAC m m)) (plus m m) (refl lzero nat (plus m m))) (aop--o--op lzero nat O plusAC m O) (let-clause-1704 m posm m m)) (times m O) (times-n-O m)) (times m (S O)) (let-clause-1692 m posm m m O)) (aop--o--op lzero nat O plusAC m O) (let-clause-1704 m posm m m)) (times m O) (times-n-O m)) (times m (S O)) (let-clause-1692 m posm m m O)) (times m (aop--o--op lzero nat O plusAC (S O) (S O))) (rewrite-l lzero lzero nat (plus (times m (S O)) (times m (S O))) (λ (X-- : nat) -> eq lzero nat (times m (aop--o--op lzero nat O plusAC (S O) (S O))) X--) (rewrite-l lzero lzero nat (plus (S O) (S O)) (λ (X-- : nat) -> eq lzero nat (times m X--) (plus (times m (S O)) (times m (S O)))) (distributive-times-plus m (S O) (S O)) (aop--o--op lzero nat O plusAC (S O) (S O)) (refl lzero nat (plus (S O) (S O)))) (aop--o--op lzero nat O plusAC (times m (S O)) (times m (S O))) (refl lzero nat (plus (times m (S O)) (times m (S O)))))) (times (aop--o--op lzero nat O plusAC (S O) (S O)) m) (commutative-times (aop--o--op lzero nat O plusAC (S O) (S O)) m)) (S (S O)) (rewrite-l lzero lzero nat (plus (S O) (S O)) (λ (X-- : nat) -> eq lzero nat (S (S O)) X--) (rewrite-r lzero lzero nat (plus (S O) (S O)) (λ (X-- : nat) -> eq lzero nat X-- (plus (S O) (S O))) (refl lzero nat (plus (S O) (S O))) (S (S O)) (rewrite-r lzero lzero nat (plus (S O) O) (λ (X-- : nat) -> eq lzero nat (S X--) (plus (S O) (S O))) (plus-n-Sm (S O) O) (S O) (plus-n-O (S O)))) (aop--o--op lzero nat O plusAC (S O) (S O)) (refl lzero nat (plus (S O) (S O))))))) (times (fact (S m)) (fact m)) (commutative-times (fact m) (fact (S m)))) (minus (plus m m) m) (minus-plus-m-m m m)) (plus m O) (plus-n-O m)) (minus (S (times (S (S O)) m)) (S m)) (rewrite-r lzero lzero nat (minus (times (S (S O)) m) m) (λ (X-- : nat) -> eq lzero nat X-- (minus (times (S (S O)) m) m)) (refl lzero nat (minus (times (S (S O)) m) m)) (minus (S (times (S (S O)) m)) (S m)) (minus-S-S (times (S (S O)) m) m))) (bc (S (times (S (S O)) m)) (S m)) (bceq (S (times (S (S O)) m)) (S m))) (bc (S (times (S (S O)) m)) m) (bceq (S (times (S (S O)) m)) m)) (plus (bc (S (times (S (S O)) m)) (S m)) O) (plus-n-O (bc (S (times (S (S O)) m)) (S m)))) (M m) (Mdef m))) (times (bc (S (times (S (S O)) m)) (S m)) (S O)) (times-n-1 (bc (S (times (S (S O)) m)) (S m)))) (times (times (bc (S (times (S (S O)) m)) (S m)) (S O)) (S O)) (times-n-1 (times (bc (S (times (S (S O)) m)) (S m)) (S O)))) (times (bc (S (times (S (S O)) m)) m) (S O)) (times-n-1 (bc (S (times (S (S O)) m)) m))) (times (times (bc (S (times (S (S O)) m)) m) (S O)) (S O)) (times-n-1 (times (bc (S (times (S (S O)) m)) m) (S O)))) (exp (S O) (S m)) (exp-1-n (S m))) (exp (S O) (minus (S (times (S (S O)) m)) (S m))) (exp-1-n (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) m) (exp-1-n m)) (exp (S O) (minus (S (times (S (S O)) m)) m)) (exp-1-n (minus (S (times (S (S O)) m)) m))) (times (S (S O)) (M m)) (rewrite-r lzero lzero nat (aop--o--op lzero nat O plusAC (S O) (S O)) (λ (X-- : nat) -> eq lzero nat (times X-- (M m)) (plus (M m) (M m))) (rewrite-r lzero lzero nat (times (M m) (aop--o--op lzero nat O plusAC (S O) (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus (M m) (M m))) (rewrite-r lzero lzero nat (aop--o--op lzero nat O plusAC (times (M m) (S O)) (times (M m) (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus (M m) (M m))) (rewrite-l lzero lzero nat (aop--o--op lzero nat O plusAC (M m) (times (M m) O)) (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC X-- (times (M m) (S O))) (plus (M m) (M m))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC (aop--o--op lzero nat O plusAC (M m) X--) (times (M m) (S O))) (plus (M m) (M m))) (rewrite-l lzero lzero nat (M m) (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC X-- (times (M m) (S O))) (plus (M m) (M m))) (rewrite-l lzero lzero nat (aop--o--op lzero nat O plusAC (M m) (times (M m) O)) (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC (M m) X--) (plus (M m) (M m))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC (M m) (aop--o--op lzero nat O plusAC (M m) X--)) (plus (M m) (M m))) (rewrite-l lzero lzero nat (M m) (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC (M m) X--) (plus (M m) (M m))) (rewrite-r lzero lzero nat (aop--o--op lzero nat O plusAC (M m) (M m)) (λ (X-- : nat) -> eq lzero nat (aop--o--op lzero nat O plusAC (M m) (M m)) X--) (refl lzero nat (aop--o--op lzero nat O plusAC (M m) (M m))) (plus (M m) (M m)) (refl lzero nat (plus (M m) (M m)))) (aop--o--op lzero nat O plusAC (M m) O) (let-clause-17041 m posm (M m) (M m))) (times (M m) O) (times-n-O (M m))) (times (M m) (S O)) (let-clause-16921 m posm (M m) (M m) O)) (aop--o--op lzero nat O plusAC (M m) O) (let-clause-17041 m posm (M m) (M m))) (times (M m) O) (times-n-O (M m))) (times (M m) (S O)) (let-clause-16921 m posm (M m) (M m) O)) (times (M m) (aop--o--op lzero nat O plusAC (S O) (S O))) (rewrite-l lzero lzero nat (plus (times (M m) (S O)) (times (M m) (S O))) (λ (X-- : nat) -> eq lzero nat (times (M m) (aop--o--op lzero nat O plusAC (S O) (S O))) X--) (rewrite-l lzero lzero nat (plus (S O) (S O)) (λ (X-- : nat) -> eq lzero nat (times (M m) X--) (plus (times (M m) (S O)) (times (M m) (S O)))) (distributive-times-plus (M m) (S O) (S O)) (aop--o--op lzero nat O plusAC (S O) (S O)) (refl lzero nat (plus (S O) (S O)))) (aop--o--op lzero nat O plusAC (times (M m) (S O)) (times (M m) (S O))) (refl lzero nat (plus (times (M m) (S O)) (times (M m) (S O)))))) (times (aop--o--op lzero nat O plusAC (S O) (S O)) (M m)) (commutative-times (aop--o--op lzero nat O plusAC (S O) (S O)) (M m))) (S (S O)) (rewrite-l lzero lzero nat (plus (S O) (S O)) (λ (X-- : nat) -> eq lzero nat (S (S O)) X--) (rewrite-r lzero lzero nat (plus (S O) (S O)) (λ (X-- : nat) -> eq lzero nat X-- (plus (S O) (S O))) (refl lzero nat (plus (S O) (S O))) (S (S O)) (rewrite-r lzero lzero nat (plus (S O) O) (λ (X-- : nat) -> eq lzero nat (S X--) (plus (S O) (S O))) (plus-n-Sm (S O) O) (S O) (plus-n-O (S O)))) (aop--o--op lzero nat O plusAC (S O) (S O)) (refl lzero nat (plus (S O) (S O)))))) (times (M m) (S (S O))) (commutative-times (M m) (S (S O)))) (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) (bigop O (λ (i : nat) -> andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb i m) (eqb i (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i)))) (refl lzero nat (plus (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) (bigop O (λ (i : nat) -> andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb i m) (eqb i (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i)))))) (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) m) (exp (S O) (minus (S (times (S (S O)) m)) m))) (exp (S O) m)) (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) (bigop O (λ (i : nat) -> andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb i m) (eqb i (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i))))) (refl lzero nat (plus (times (times (bc (S (times (S (S O)) m)) m) (exp (S O) (minus (S (times (S (S O)) m)) m))) (exp (S O) m)) (aop--o--op lzero nat O plusAC (times (times (bc (S (times (S (S O)) m)) (S m)) (exp (S O) (minus (S (times (S (S O)) m)) (S m)))) (exp (S O) (S m))) (bigop O (λ (i : nat) -> andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb i m) (eqb i (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i))))))) (bigop (S (S (times (S (S O)) m))) (λ (i : nat) -> andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb i m) (eqb i (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (i : nat) -> times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i))) (pad-bigop1 (S (S (times (S (S O)) m))) O (λ (X-- : nat) -> andb (notb (eqb (S m) X--)) (andb (notb (eqb m X--)) (orb (eqb X-- m) (eqb X-- (S m))))) nat O (aop--o--op lzero nat O plusAC) (λ (X-- : nat) -> times (times (bc (S (times (S (S O)) m)) X--) (exp (S O) (minus (S (times (S (S O)) m)) X--))) (exp (S O) X--)) (le-O-n (S (S (times (S (S O)) m)))) (λ (i : nat) -> λ (X-- : le O i) -> λ (X-0 : lt i (S (S (times (S (S O)) m)))) -> eq-ind-r lzero lzero bool (eqb m i) (λ (x : bool) -> λ (X-1 : eq lzero bool x (eqb m i)) -> eq lzero bool (andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb x (eqb i (S m))))) false) (eq-ind-r lzero lzero bool (eqb (S m) i) (λ (x : bool) -> λ (X-1 : eq lzero bool x (eqb (S m) i)) -> eq lzero bool (andb (notb (eqb (S m) i)) (andb (notb (eqb m i)) (orb (eqb m i) x))) false) (match-bool lzero (λ (X-1 : bool) -> eq lzero bool (andb (notb (eqb (S m) i)) (andb (notb X-1) (orb X-1 (eqb (S m) i)))) false) (match-bool lzero (λ (X-1 : bool) -> eq lzero bool (andb (notb X-1) (andb (notb true) (orb true X-1))) false) (refl lzero bool (andb (notb true) (andb (notb true) (orb true true)))) (refl lzero bool (andb (notb false) (andb (notb true) (orb true false)))) (eqb (S m) i)) (match-bool lzero (λ (X-1 : bool) -> eq lzero bool (andb (notb X-1) (andb (notb false) (orb false X-1))) false) (refl lzero bool (andb (notb true) (andb (notb false) (orb false true)))) (refl lzero bool (andb (notb false) (andb (notb false) (orb false false)))) (eqb (S m) i)) (eqb m i)) (eqb i (S m)) (eqb-sym i (S m))) (eqb i m) (eqb-sym i m)))) (bigop (S (S (times (S (S O)) m))) (λ (x : nat) -> andb (notb (eqb m x)) (orb (eqb x m) (eqb x (S m)))) nat O (aop--o--op lzero nat O plusAC) (λ (x : nat) -> times (times (bc (S (times (S (S O)) m)) x) (exp (S O) (minus (S (times (S (S O)) m)) x))) (exp (S O) x))) (bigop-diff (λ (X-- : nat) -> andb (notb (eqb m X--)) (orb (eqb X-- m) (eqb X-- (S m)))) nat O plusAC (λ (X-- : nat) -> times (times (bc (S (times (S (S O)) m)) X--) (exp (S O) (minus (S (times (S (S O)) m)) X--))) (exp (S O) X--)) (S m) (S (S (times (S (S O)) m))) (le-S-S (S m) (S (times (S (S O)) m)) (le-S-S m (times (S (S O)) m) (eq-coerc lzero (le (minus (plus m (times m (plus (S O) O))) (times m (plus (S O) O))) (plus m (times m (plus (S O) O)))) (le m (times (S (S O)) m)) (minus-le (plus m (times m (plus (S O) O))) (times m (plus (S O) O))) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus m (times m (plus (S O) O)))) (le m (times (S (S O)) m))) (rewrite-r lzero (lsuc lzero) nat (plus (S O) (S O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m (plus m (times m (plus (S O) O)))) (le m (times X-- m))) (rewrite-r lzero (lsuc lzero) nat (times m (plus (S O) (S O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m (plus m (times m (plus (S O) O)))) (le m X--)) (rewrite-r lzero (lsuc lzero) nat (times m (plus (S O) (S O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m X--) (le m (times m (plus (S O) (S O))))) (refl (lsuc lzero) (Set (lzero)) (le m (times m (plus (S O) (S O))))) (plus m (times m (plus (S O) O))) (rewrite-l lzero lzero nat (S (plus (S O) O)) (λ (X-- : nat) -> eq lzero nat (plus m (times m (plus (S O) O))) (times m X--)) (times-n-Sm m (plus (S O) O)) (plus (S O) (S O)) (plus-n-Sm (S O) O))) (times (plus (S O) (S O)) m) (commutative-times (plus (S O) (S O)) m)) (S (S O)) (rewrite-r lzero lzero nat (plus (S O) (S O)) (λ (X-- : nat) -> eq lzero nat X-- (plus (S O) (S O))) (refl lzero nat (plus (S O) (S O))) (S (S O)) (rewrite-r lzero lzero nat (plus (S O) O) (λ (X-- : nat) -> eq lzero nat (S X--) (plus (S O) (S O))) (plus-n-Sm (S O) O) (S O) (plus-n-O (S O))))) (minus (plus m (times m (plus (S O) O))) (times m (plus (S O) O))) (minus-plus-m-m m (times m (plus (S O) O))))))) (eq-ind-r lzero lzero bool (eqb m (S m)) (λ (x : bool) -> λ (X-- : eq lzero bool x (eqb m (S m))) -> eq lzero bool (andb (notb (eqb m (S m))) (orb x (eqb (S m) (S m)))) true) (eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero bool (andb (notb (eqb m (S m))) (orb (eqb m (S m)) x)) true) (eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool (andb (notb x) (orb x true)) true) (refl lzero bool (andb (notb false) (orb false true))) (eqb m (S m)) (not-eq-to-eqb-false m (S m) (not-to-not lzero (eq lzero nat m (S m)) (eq lzero nat m (S m)) (λ (auto : eq lzero nat m (S m)) -> rewrite-l lzero lzero nat m (λ (X-- : nat) -> eq lzero nat m X--) (refl lzero nat m) (S m) auto) (not-eq-n-Sn m)))) (eqb (S m) (S m)) (eq-to-eqb-true (S m) (S m) (refl lzero nat (S m)))) (eqb (S m) m) (eqb-sym (S m) m)))) (bigop (S (S (times (S (S O)) m))) (λ (x : nat) -> orb (eqb x m) (eqb x (S m))) nat O (aop--o--op lzero nat O plusAC) (λ (x : nat) -> times (times (bc (S (times (S (S O)) m)) x) (exp (S O) (minus (S (times (S (S O)) m)) x))) (exp (S O) x))) (bigop-diff (λ (X-- : nat) -> orb (eqb X-- m) (eqb X-- (S m))) nat O plusAC (λ (X-- : nat) -> times (times (bc (S (times (S (S O)) m)) X--) (exp (S O) (minus (S (times (S (S O)) m)) X--))) (exp (S O) X--)) m (S (S (times (S (S O)) m))) (le-S (S m) (S (times (S (S O)) m)) (le-S-S m (times (S (S O)) m) (eq-coerc lzero (le (minus (plus m (times m (plus (S O) O))) (times m (plus (S O) O))) (plus m (times m (plus (S O) O)))) (le m (times (S (S O)) m)) (minus-le (plus m (times m (plus (S O) O))) (times m (plus (S O) O))) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus m (times m (plus (S O) O)))) (le m (times (S (S O)) m))) (rewrite-r lzero (lsuc lzero) nat (plus (S O) (S O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m (plus m (times m (plus (S O) O)))) (le m (times X-- m))) (rewrite-r lzero (lsuc lzero) nat (times m (plus (S O) (S O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m (plus m (times m (plus (S O) O)))) (le m X--)) (rewrite-r lzero (lsuc lzero) nat (times m (plus (S O) (S O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m X--) (le m (times m (plus (S O) (S O))))) (refl (lsuc lzero) (Set (lzero)) (le m (times m (plus (S O) (S O))))) (plus m (times m (plus (S O) O))) (rewrite-l lzero lzero nat (S (plus (S O) O)) (λ (X-- : nat) -> eq lzero nat (plus m (times m (plus (S O) O))) (times m X--)) (times-n-Sm m (plus (S O) O)) (plus (S O) (S O)) (plus-n-Sm (S O) O))) (times (plus (S O) (S O)) m) (commutative-times (plus (S O) (S O)) m)) (S (S O)) (rewrite-r lzero lzero nat (plus (S O) (S O)) (λ (X-- : nat) -> eq lzero nat X-- (plus (S O) (S O))) (refl lzero nat (plus (S O) (S O))) (S (S O)) (rewrite-r lzero lzero nat (plus (S O) O) (λ (X-- : nat) -> eq lzero nat (S X--) (plus (S O) (S O))) (plus-n-Sm (S O) O) (S O) (plus-n-O (S O))))) (minus (plus m (times m (plus (S O) O))) (times m (plus (S O) O))) (minus-plus-m-m m (times m (plus (S O) O))))))) (eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero bool (orb x (eqb m (S m))) true) (refl lzero bool (orb true (eqb m (S m)))) (eqb m m) (eq-to-eqb-true m m (refl lzero nat m))))) (lt-sigma-p (S (S (times (S (S O)) m))) (λ (X-- : nat) -> orb (eqb X-- m) (eqb X-- (S m))) (λ (X-- : nat) -> true) (λ (X-- : nat) -> times (times (bc (S (times (S (S O)) m)) X--) (exp (S O) (minus (S (times (S (S O)) m)) X--))) (exp (S O) X--)) (λ (X-- : nat) -> times (times (bc (S (times (S (S O)) m)) X--) (exp (S O) (minus (S (times (S (S O)) m)) X--))) (exp (S O) X--)) (λ (i : nat) -> λ (auto : lt i (S (S (times (S (S O)) m)))) -> λ (auto' : eq lzero bool (orb (eqb i m) (eqb i (S m))) true) -> refl lzero bool true) (λ (i : nat) -> λ (lti : lt i (S (S (times (S (S O)) m)))) -> λ (Hi : eq lzero bool (orb (eqb i m) (eqb i (S m))) true) -> le-n (times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i))) (ex-intro lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i (S (S (times (S (S O)) m)))) (Or lzero lzero (And lzero lzero (eq lzero bool (orb (eqb i m) (eqb i (S m))) true) (lt (times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i)) (times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i)))) (And lzero lzero (And lzero lzero (eq lzero bool (orb (eqb i m) (eqb i (S m))) false) (eq lzero bool true true)) (lt O (times (times (bc (S (times (S (S O)) m)) i) (exp (S O) (minus (S (times (S (S O)) m)) i))) (exp (S O) i)))))) O (conj lzero lzero (lt O (S (S (times (S (S O)) m)))) (Or lzero lzero (And lzero lzero (eq lzero bool (orb (eqb O m) (eqb O (S m))) true) (lt (times (times (bc (S (times (S (S O)) m)) O) (exp (S O) (minus (S (times (S (S O)) m)) O))) (exp (S O) O)) (times (times (bc (S (times (S (S O)) m)) O) (exp (S O) (minus (S (times (S (S O)) m)) O))) (exp (S O) O)))) (And lzero lzero (And lzero lzero (eq lzero bool (orb (eqb O m) (eqb O (S m))) false) (eq lzero bool true true)) (lt O (times (times (bc (S (times (S (S O)) m)) O) (exp (S O) (minus (S (times (S (S O)) m)) O))) (exp (S O) O))))) (lt-O-S (S (times (S (S O)) m))) (or-intror lzero lzero (And lzero lzero (eq lzero bool (orb (eqb O m) (eqb O (S m))) true) (lt (times (times (bc (S (times (S (S O)) m)) O) (exp (S O) (minus (S (times (S (S O)) m)) O))) (exp (S O) O)) (times (times (bc (S (times (S (S O)) m)) O) (exp (S O) (minus (S (times (S (S O)) m)) O))) (exp (S O) O)))) (And lzero lzero (And lzero lzero (eq lzero bool (orb (eqb O m) (eqb O (S m))) false) (eq lzero bool true true)) (lt O (times (times (bc (S (times (S (S O)) m)) O) (exp (S O) (minus (S (times (S (S O)) m)) O))) (exp (S O) O)))) (conj lzero lzero (And lzero lzero (eq lzero bool (orb (eqb O m) (eqb O (S m))) false) (eq lzero bool true true)) (lt O (times (times (bc (S (times (S (S O)) m)) O) (exp (S O) (minus (S (times (S (S O)) m)) O))) (exp (S O) O))) (conj lzero lzero (eq lzero bool (orb (eqb O m) (eqb O (S m))) false) (eq lzero bool true true) (eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool (orb (eqb O m) x) false) (eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool (orb x false) false) (refl lzero bool (orb false false)) (eqb O m) (not-eq-to-eqb-false O m (lt-to-not-eq O m posm))) (eqb O (S m)) (not-eq-to-eqb-false O (S m) (not-eq-O-S m))) (refl lzero bool true)) (eq-ind-r lzero lzero nat (S O) (λ (x : nat) -> λ (X-- : eq lzero nat x (S O)) -> lt O (times (times x (exp (S O) (minus (S (times (S (S O)) m)) O))) (exp (S O) O))) (eq-ind lzero lzero nat (S O) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S O) x-1) -> lt O (times (times (S O) x-1) (exp (S O) O))) (eq-ind lzero lzero nat (S O) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S O) x-1) -> lt O (times (times (S O) (S O)) x-1)) (le-n (S O)) (exp (S O) O) (exp-1-n O)) (exp (S O) (minus (S (times (S (S O)) m)) O)) (exp-1-n (minus (S (times (S (S O)) m)) O))) (bc (S (times (S (S O)) m)) O) (bc-n-O (S (times (S (S O)) m)))))))))) (exp (plus (S O) (S O)) (S (times (S (S O)) m))) (binomial-law (S O) (S O) (S (times (S (S O)) m)))) (S (S O)) (rewrite-r lzero lzero nat (plus (S O) (S O)) (λ (X-- : nat) -> eq lzero nat X-- (plus (S O) (S O))) (refl lzero nat (plus (S O) (S O))) (S (S O)) (rewrite-r lzero lzero nat (plus (S O) O) (λ (X-- : nat) -> eq lzero nat (S X--) (plus (S O) (S O))) (plus-n-Sm (S O) O) (S O) (plus-n-O (S O))))) (times (exp (S (S O)) (times (S (S O)) m)) (S (S O))) (refl lzero nat (exp (S (S O)) (S (times (S (S O)) m)))))