-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmatita-arithmetics-chebyshev-factorization.agda
115 lines (81 loc) · 125 KB
/
matita-arithmetics-chebyshev-factorization.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
open import Agda.Primitive
open import matita-arithmetics-minimization
open import matita-arithmetics-ord
open import matita-arithmetics-sigma-pi
open import matita-arithmetics-primes
open import matita-arithmetics-bigops
open import matita-arithmetics-log
open import matita-basics-bool
open import matita-arithmetics-div-and-mod
open import matita-basics-logic
open import matita-arithmetics-factorial
open import matita-arithmetics-exp
open import matita-arithmetics-nat
eq-pi-p-primeb-divides-b : (n : nat) -> (m : nat) -> eq lzero nat (bigop n (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))) (bigop n (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (ord m p)))
eq-pi-p-primeb-divides-b = λ (n : nat) -> λ (m : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat (bigop X-x-365 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))) (bigop X-x-365 (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) (refl lzero nat (bigop O (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) (λ (n1 : nat) -> λ (Hind : eq lzero nat (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))) (bigop n1 (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) -> match-Or lzero lzero (eq lzero bool (primeb n1) true) (eq lzero bool (primeb n1) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (primeb n1) true) (eq lzero bool (primeb n1) false)) -> eq lzero nat (bigop (S n1) (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))) (bigop (S n1) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) (λ (Hprime : eq lzero bool (primeb n1) true) -> eq-ind-r lzero lzero nat (times (exp n1 (ord m n1)) (bigop n1 (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (ord m i)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp n1 (ord m n1)) (bigop n1 (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (ord m i))))) -> eq lzero nat (bigop (S n1) (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))) x) (match-Or lzero lzero (eq lzero bool (dividesb n1 m) true) (eq lzero bool (dividesb n1 m) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (dividesb n1 m) true) (eq lzero bool (dividesb n1 m) false)) -> eq lzero nat (bigop (S n1) (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))) (times (exp n1 (ord m n1)) (bigop n1 (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (ord m i))))) (λ (Hdivides : eq lzero bool (dividesb n1 m) true) -> eq-ind-r lzero lzero nat (times (exp n1 (ord m n1)) (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp n1 (ord m n1)) (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))))) -> eq lzero nat x (times (exp n1 (ord m n1)) (bigop n1 (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (ord m i))))) (eq-f lzero lzero nat nat (times (exp n1 (ord m n1))) (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (bigop n1 (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (ord m i))) Hind) (bigop (S n1) (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (bigop-Strue n1 (λ (X-- : nat) -> andb (primeb X--) (dividesb X-- m)) nat (S O) times (λ (X-- : nat) -> exp X-- (ord m X--)) (true-to-andb-true (primeb n1) (dividesb n1 m) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb n1) Hprime) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (dividesb n1 m) Hdivides)))) (λ (Hdivides : eq lzero bool (dividesb n1 m) false) -> eq-ind-r lzero lzero nat (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i)))) -> eq lzero nat x (times (exp n1 (ord m n1)) (bigop n1 (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (ord m i))))) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (times (exp n1 x) (bigop n1 (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (ord m i))))) (rewrite-l lzero lzero nat (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))) (λ (X-- : nat) -> eq lzero nat (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (times (S O) X--)) (rewrite-l lzero lzero nat (times (S O) (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) (λ (X-- : nat) -> eq lzero nat X-- (times (S O) (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))))) (refl lzero nat (times (S O) (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))))) (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))) (rewrite-r lzero lzero nat (times (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))) (S O)) (λ (X-- : nat) -> eq lzero nat (times (S O) (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) X--) (commutative-times (S O) (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))) (times-n-1 (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p)))))) (bigop n1 (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (ord m p))) Hind) (ord m n1) (not-divides-to-ord-O n1 m (primeb-true-to-prime n1 (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb n1) Hprime)) (dividesb-false-to-not-divides n1 m (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (dividesb n1 m) Hdivides)))) (bigop (S n1) (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (bigop-Sfalse n1 (λ (X-- : nat) -> andb (primeb X--) (dividesb X-- m)) nat (S O) times (λ (X-- : nat) -> exp X-- (ord m X--)) (eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero bool (andb x (dividesb n1 m)) false) (eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool (andb true x) false) (refl lzero bool (andb true false)) (dividesb n1 m) Hdivides) (primeb n1) Hprime))) (true-or-false (dividesb n1 m))) (bigop (S n1) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (bigop-Strue n1 primeb nat (S O) times (λ (X-- : nat) -> exp X-- (ord m X--)) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb n1) Hprime))) (λ (Hprime : eq lzero bool (primeb n1) false) -> eq-ind-r lzero lzero nat (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i)))) -> eq lzero nat x (bigop (S n1) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) (eq-ind-r lzero lzero nat (bigop n1 (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop n1 (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (ord m i)))) -> eq lzero nat (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) x) (rewrite-l lzero lzero nat (bigop n1 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p))) (λ (X-- : nat) -> eq lzero nat (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) X--) (refl lzero nat (bigop n1 (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i)))) (bigop n1 (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (ord m p))) Hind) (bigop (S n1) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (bigop-Sfalse n1 primeb nat (S O) times (λ (X-- : nat) -> exp X-- (ord m X--)) (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (primeb n1) Hprime))) (bigop (S n1) (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (bigop-Sfalse n1 (λ (X-- : nat) -> andb (primeb X--) (dividesb X-- m)) nat (S O) times (λ (X-- : nat) -> exp X-- (ord m X--)) (eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool (andb x (dividesb n1 m)) false) (refl lzero bool (andb false (dividesb n1 m))) (primeb n1) Hprime))) (true-or-false (primeb n1))) n
lt-1-max-prime : (n : nat) -> (X-- : lt (S O) n) -> lt (S O) (max'' (S n) (λ (i : nat) -> andb (primeb i) (dividesb i n)))
lt-1-max-prime = λ (n : nat) -> λ (lt1n : lt (S O) n) -> lt-to-le-to-lt (S O) (smallest-factor n) (max'' (S n) (λ (i : nat) -> andb (primeb i) (dividesb i n))) (lt-SO-smallest-factor n lt1n) (true-to-le-max (λ (i : nat) -> andb (primeb i) (dividesb i n)) (S n) (smallest-factor n) (le-S-S (smallest-factor n) n (le-smallest-factor-n n)) (true-to-andb-true (primeb (smallest-factor n)) (dividesb (smallest-factor n) n) (prime-to-primeb-true (smallest-factor n) (prime-smallest-factor-n n lt1n)) (divides-to-dividesb-true (smallest-factor n) n (lt-O-smallest-factor n (lt-to-le (S O) n lt1n)) (divides-smallest-factor-n n (lt-to-le (S O) n lt1n)))))
lt-max-to-pi-p-primeb : (q : nat) -> (m : nat) -> (X-- : lt O m) -> (X--1 : lt (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) q) -> eq lzero nat m (bigop q (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p)))
lt-max-to-pi-p-primeb = λ (q : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (m : nat) -> (X-- : lt O m) -> (X--1 : lt (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) X-x-365) -> eq lzero nat m (bigop X-x-365 (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) (λ (m : nat) -> λ (posm : lt O m) -> λ (Hmax : lt (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) O) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat m (S O)) (absurd lzero (lt (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) O) Hmax (not-le-Sn-O (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m)))))) (λ (n : nat) -> λ (Hind : (m : nat) -> (X-- : lt O m) -> (X--1 : lt (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) n) -> eq lzero nat m (bigop n (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) -> λ (m : nat) -> λ (posm : lt O m) -> λ (Hmax : lt (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) (S n)) -> match-Or lzero lzero (eq lzero bool (andb (primeb n) (dividesb n m)) true) (eq lzero bool (andb (primeb n) (dividesb n m)) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (andb (primeb n) (dividesb n m)) true) (eq lzero bool (andb (primeb n) (dividesb n m)) false)) -> eq lzero nat m (bigop (S n) (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) (λ (Hcase : eq lzero bool (andb (primeb n) (dividesb n m)) true) -> eq-ind-r lzero lzero nat (times (exp n (ord m n)) (bigop n (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp n (ord m n)) (bigop n (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))))) -> eq lzero nat m x) (eq-ind-r lzero lzero nat (times (exp n (ord m n)) (ord-rem m n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp n (ord m n)) (ord-rem m n))) -> eq lzero nat x (times (exp n (ord m n)) (bigop n (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))))) (eq-f lzero lzero nat nat (times (exp n (ord m n))) (ord-rem m n) (bigop n (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (eq-ind-r lzero lzero nat (bigop n (λ (p : nat) -> andb (primeb p) (dividesb p (ord-rem m n))) nat (S O) times (λ (p : nat) -> exp p (ord (ord-rem m n) p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop n (λ (p : nat) -> andb (primeb p) (dividesb p (ord-rem m n))) nat (S O) times (λ (p : nat) -> exp p (ord (ord-rem m n) p)))) -> eq lzero nat x (bigop n (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i)))) (same-bigop n (λ (X-- : nat) -> andb (primeb X--) (dividesb X-- (ord-rem m n))) (λ (X-- : nat) -> andb (primeb X--) (dividesb X-- m)) nat (S O) times (λ (X-- : nat) -> exp X-- (ord (ord-rem m n) X--)) (λ (X-- : nat) -> exp X-- (ord m X--)) (λ (x : nat) -> λ (ltxn : lt x n) -> match-Or lzero lzero (eq lzero bool (primeb x) true) (eq lzero bool (primeb x) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (primeb x) true) (eq lzero bool (primeb x) false)) -> eq lzero bool (andb (primeb x) (dividesb x (ord-rem m n))) (andb (primeb x) (dividesb x m))) (λ (Hx : eq lzero bool (primeb x) true) -> eq-ind-r lzero lzero bool true (λ (x0 : bool) -> λ (X-- : eq lzero bool x0 true) -> eq lzero bool (andb x0 (dividesb x (ord-rem m n))) (andb x0 (dividesb x m))) (match-Or lzero lzero (eq lzero bool (dividesb x (ord-rem m n)) true) (eq lzero bool (dividesb x (ord-rem m n)) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (dividesb x (ord-rem m n)) true) (eq lzero bool (dividesb x (ord-rem m n)) false)) -> eq lzero bool (andb true (dividesb x (ord-rem m n))) (andb true (dividesb x m))) (λ (Hx1 : eq lzero bool (dividesb x (ord-rem m n)) true) -> eq-ind-r lzero lzero bool true (λ (x0 : bool) -> λ (X-- : eq lzero bool x0 true) -> eq lzero bool (andb true x0) (andb true (dividesb x m))) (sym-eq lzero bool (andb true (dividesb x m)) (andb true true) (divides-to-dividesb-true x m (prime-to-lt-O x (primeb-true-to-prime x (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb x) Hx))) (transitive-divides x (ord-rem m n) m (dividesb-true-to-divides x (ord-rem m n) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (dividesb x (ord-rem m n)) Hx1)) (divides-ord-rem n m (transitive-lt (S O) x n (prime-to-lt-SO x (primeb-true-to-prime x (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb x) Hx))) ltxn) posm)))) (dividesb x (ord-rem m n)) Hx1) (λ (Hx1 : eq lzero bool (dividesb x (ord-rem m n)) false) -> eq-ind-r lzero lzero bool false (λ (x0 : bool) -> λ (X-- : eq lzero bool x0 false) -> eq lzero bool (andb true x0) (andb true (dividesb x m))) (sym-eq lzero bool (andb true (dividesb x m)) (andb true false) (not-divides-to-dividesb-false x m (prime-to-lt-O x (primeb-true-to-prime x (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb x) Hx))) (ord-O-to-not-divides x m posm (primeb-true-to-prime x (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb x) Hx)) (eq-ind lzero lzero nat (ord (ord-rem m n) x) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (ord (ord-rem m n) x) x-1) -> eq lzero nat x-1 O) (not-divides-to-ord-O x (ord-rem m n) (primeb-true-to-prime x (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb x) Hx)) (dividesb-false-to-not-divides x (ord-rem m n) (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (dividesb x (ord-rem m n)) Hx1))) (ord m x) (ord-ord-rem n x m posm (primeb-true-to-prime n (andb-true-l (primeb n) (dividesb n m) Hcase)) (primeb-true-to-prime x (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb x) Hx)) ltxn))))) (dividesb x (ord-rem m n)) Hx1) (true-or-false (dividesb x (ord-rem m n)))) (primeb x) Hx) (λ (Hx : eq lzero bool (primeb x) false) -> eq-ind-r lzero lzero bool false (λ (x0 : bool) -> λ (X-- : eq lzero bool x0 false) -> eq lzero bool (andb x0 (dividesb x (ord-rem m n))) (andb x0 (dividesb x m))) (refl lzero bool (andb false (dividesb x (ord-rem m n)))) (primeb x) Hx) (true-or-false (primeb x))) (λ (x : nat) -> λ (ltxn : lt x n) -> λ (Hx : eq lzero bool (andb (primeb x) (dividesb x (ord-rem m n))) true) -> eq-f lzero lzero nat nat (exp x) (ord (ord-rem m n) x) (ord m x) (ord-ord-rem n x m posm (primeb-true-to-prime n (andb-true-l (primeb n) (dividesb n m) Hcase)) (primeb-true-to-prime x (andb-true-l (primeb x) (dividesb x (ord-rem m n)) Hx)) ltxn))) (ord-rem m n) (Hind (ord-rem m n) (lt-O-ord-rem n m (prime-to-lt-SO n (primeb-true-to-prime n (andb-true-l (primeb n) (dividesb n m) Hcase))) posm) (not-eq-to-le-to-lt (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) n (Or-ind lzero lzero lzero (And lzero lzero (ex lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i (S (ord-rem m n))) (eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) true))) (eq lzero bool (andb (primeb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n))))) (dividesb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) (ord-rem m n))) true)) (And lzero lzero ((i : nat) -> (X-- : lt i (S (ord-rem m n))) -> eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) false) (eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) O)) (λ (X-x-170 : Or lzero lzero (And lzero lzero (ex lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i (S (ord-rem m n))) (eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) true))) (eq lzero bool (andb (primeb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n))))) (dividesb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) (ord-rem m n))) true)) (And lzero lzero ((i : nat) -> (X-- : lt i (S (ord-rem m n))) -> eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) false) (eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) O))) -> Not lzero (eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) n)) (λ (X-clearme : And lzero lzero (ex lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i (S (ord-rem m n))) (eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) true))) (eq lzero bool (andb (primeb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n))))) (dividesb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) (ord-rem m n))) true)) -> match-And lzero lzero (ex lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i (S (ord-rem m n))) (eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) true))) (eq lzero bool (andb (primeb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n))))) (dividesb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) (ord-rem m n))) true) lzero (λ (X-- : And lzero lzero (ex lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i (S (ord-rem m n))) (eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) true))) (eq lzero bool (andb (primeb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n))))) (dividesb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) (ord-rem m n))) true)) -> Not lzero (eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) n)) (λ (Hex : ex lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i (S (ord-rem m n))) (eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) true))) -> λ (Hord-rem : eq lzero bool (andb (primeb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n))))) (dividesb (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) (ord-rem m n))) true) -> match-ex lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i (S (ord-rem m n))) (eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) true)) lzero (λ (X-- : ex lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i (S (ord-rem m n))) (eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) true))) -> Not lzero (eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) n)) (λ (x : nat) -> λ (X-clearme0 : And lzero lzero (lt x (S (ord-rem m n))) (eq lzero bool (andb (primeb x) (dividesb x (ord-rem m n))) true)) -> match-And lzero lzero (lt x (S (ord-rem m n))) (eq lzero bool (andb (primeb x) (dividesb x (ord-rem m n))) true) lzero (λ (X-- : And lzero lzero (lt x (S (ord-rem m n))) (eq lzero bool (andb (primeb x) (dividesb x (ord-rem m n))) true)) -> Not lzero (eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) n)) (λ (H6 : lt x (S (ord-rem m n))) -> λ (H7 : eq lzero bool (andb (primeb x) (dividesb x (ord-rem m n))) true) -> nmk lzero (eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) n) (λ (H : eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) n) -> eq-ind-r lzero lzero nat n (λ (x0 : nat) -> λ (X-- : eq lzero nat x0 n) -> (X--1 : eq lzero bool (andb (primeb x0) (dividesb x0 (ord-rem m n))) true) -> False lzero) (λ (Hn : eq lzero bool (andb (primeb n) (dividesb n (ord-rem m n))) true) -> absurd lzero (divides n (ord-rem m n)) (dividesb-true-to-divides n (ord-rem m n) (andb-true-r (primeb n) (dividesb n (ord-rem m n)) Hn)) (not-divides-ord-rem m n posm (prime-to-lt-SO n (primeb-true-to-prime n (andb-true-l (primeb n) (dividesb n (ord-rem m n)) Hn))))) (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) H Hord-rem)) X-clearme0) Hex) X-clearme) (λ (X-clearme : And lzero lzero ((i : nat) -> (X-- : lt i (S (ord-rem m n))) -> eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) false) (eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) O)) -> match-And lzero lzero ((i : nat) -> (X-- : lt i (S (ord-rem m n))) -> eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) false) (eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) O) lzero (λ (X-- : And lzero lzero ((i : nat) -> (X-- : lt i (S (ord-rem m n))) -> eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) false) (eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) O)) -> Not lzero (eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) n)) (λ (Hall : (i : nat) -> (X-- : lt i (S (ord-rem m n))) -> eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) false) -> λ (Hmax0 : eq lzero nat (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) O) -> eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> Not lzero (eq lzero nat x n)) (lt-to-not-eq O n (prime-to-lt-O n (primeb-true-to-prime n (andb-true-l (primeb n) (dividesb n m) Hcase)))) (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) Hmax0) X-clearme) (exists-max-forall-false (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n))) (S (ord-rem m n)))) (transitive-le (max'' (S (ord-rem m n)) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) n (le-to-le-max (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n))) (S (ord-rem m n)) (S m) (le-S-S (ord-rem m n) m (divides-to-le (ord-rem m n) m posm (divides-ord-rem n m (prime-to-lt-SO n (primeb-true-to-prime n (andb-true-l (primeb n) (dividesb n m) Hcase))) posm)))) (transitive-le (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n)))) (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) n (le-max-f-max-g (λ (i : nat) -> andb (primeb i) (dividesb i (ord-rem m n))) (λ (i : nat) -> andb (primeb i) (dividesb i m)) (S m) (λ (i : nat) -> λ (ltim : lt i (S m)) -> λ (Hi : eq lzero bool (andb (primeb i) (dividesb i (ord-rem m n))) true) -> match-Or lzero lzero (eq lzero bool (primeb i) true) (eq lzero bool (primeb i) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (primeb i) true) (eq lzero bool (primeb i) false)) -> eq lzero bool (andb (primeb i) (dividesb i m)) true) (λ (Hprimei : eq lzero bool (primeb i) true) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero bool (andb x (dividesb i m)) true) (divides-to-dividesb-true i m (prime-to-lt-O i (primeb-true-to-prime i (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb i) Hprimei))) (transitive-divides i (ord-rem m n) m (dividesb-true-to-divides i (ord-rem m n) (andb-true-r (primeb i) (dividesb i (ord-rem m n)) Hi)) (divides-ord-rem n m (prime-to-lt-SO n (primeb-true-to-prime n (andb-true-l (primeb n) (dividesb n m) Hcase))) posm))) (primeb i) Hprimei) (λ (Hprimei : eq lzero bool (primeb i) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool (andb x (dividesb i m)) true) (eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> (X--1 : eq lzero bool (andb x (dividesb i (ord-rem m n))) true) -> eq lzero bool (andb false (dividesb i m)) true) (λ (Hi0 : eq lzero bool (andb false (dividesb i (ord-rem m n))) true) -> Hi0) (primeb i) Hprimei Hi) (primeb i) Hprimei) (true-or-false (primeb i)))) (le-S-S-to-le (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) n Hmax))))))) m (exp-ord n m (prime-to-lt-SO n (primeb-true-to-prime n (andb-true-l (primeb n) (dividesb n m) Hcase))) posm)) (bigop (S n) (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (bigop-Strue n (λ (X-- : nat) -> andb (primeb X--) (dividesb X-- m)) nat (S O) times (λ (X-- : nat) -> exp X-- (ord m X--)) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (andb (primeb n) (dividesb n m)) Hcase))) (λ (Hcase : eq lzero bool (andb (primeb n) (dividesb n m)) false) -> match-Or lzero lzero (lt (S O) m) (eq lzero nat (S O) m) lzero (λ (X-- : Or lzero lzero (lt (S O) m) (eq lzero nat (S O) m)) -> eq lzero nat m (bigop (S n) (λ (p : nat) -> andb (primeb p) (dividesb p m)) nat (S O) times (λ (p : nat) -> exp p (ord m p)))) (λ (Hm : lt (S O) m) -> eq-ind-r lzero lzero nat (bigop n (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop n (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i)))) -> eq lzero nat m x) (Hind m posm (false-to-lt-max (λ (i : nat) -> andb (primeb i) (dividesb i m)) n (S m) (lt-to-le-to-lt O (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) n (lt-to-le (S O) (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) (lt-1-max-prime m Hm)) (le-S-S-to-le (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) n Hmax)) (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (andb (primeb n) (dividesb n m)) Hcase) (le-S-S-to-le (max'' (S m) (λ (i : nat) -> andb (primeb i) (dividesb i m))) n Hmax))) (bigop (S n) (λ (i : nat) -> andb (primeb i) (dividesb i m)) nat (S O) times (λ (i : nat) -> exp i (ord m i))) (bigop-Sfalse n (λ (X-- : nat) -> andb (primeb X--) (dividesb X-- m)) nat (S O) times (λ (X-- : nat) -> exp X-- (ord m X--)) Hcase)) (λ (Hm : eq lzero nat (S O) m) -> eq-ind lzero lzero nat (S O) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S O) x-1) -> eq lzero nat x-1 (bigop (S n) (λ (p : nat) -> andb (primeb p) (dividesb p x-1)) nat (S O) times (λ (p : nat) -> exp p (ord x-1 p)))) (eq-ind lzero lzero nat (bigop (S n) (λ (i : nat) -> false) nat (S O) times (λ (i : nat) -> exp i (ord (S O) i))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bigop (S n) (λ (i : nat) -> false) nat (S O) times (λ (i : nat) -> exp i (ord (S O) i))) x-1) -> eq lzero nat x-1 (bigop (S n) (λ (p : nat) -> andb (primeb p) (dividesb p (S O))) nat (S O) times (λ (p : nat) -> exp p (ord (S O) p)))) (same-bigop (S n) (λ (X-- : nat) -> false) (λ (X-- : nat) -> andb (primeb X--) (dividesb X-- (S O))) nat (S O) times (λ (X-- : nat) -> exp X-- (ord (S O) X--)) (λ (X-- : nat) -> exp X-- (ord (S O) X--)) (λ (i : nat) -> λ (lein : lt i (S n)) -> match-Or lzero lzero (eq lzero bool (primeb i) true) (eq lzero bool (primeb i) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (primeb i) true) (eq lzero bool (primeb i) false)) -> eq lzero bool false (andb (primeb i) (dividesb i (S O)))) (λ (primei : eq lzero bool (primeb i) true) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero bool false (andb x (dividesb i (S O)))) (sym-eq lzero bool (andb true (dividesb i (S O))) false (not-divides-to-dividesb-false i (S O) (prime-to-lt-O i (primeb-true-to-prime i (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb i) primei))) (nmk lzero (divides i (S O)) (λ (divi : divides i (S O)) -> absurd lzero (lt (S O) i) (prime-to-lt-SO i (primeb-true-to-prime i primei)) (le-to-not-lt i (S O) (divides-to-le i (S O) (lt-O-S O) divi)))))) (primeb i) primei) (λ (primei : eq lzero bool (primeb i) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool false (andb x (dividesb i (S O)))) (refl lzero bool false) (primeb i) primei) (true-or-false (primeb i))) (λ (i : nat) -> λ (auto : lt i (S n)) -> λ (auto' : eq lzero bool false true) -> rewrite-r lzero lzero nat m (λ (X-- : nat) -> eq lzero nat (exp i (ord X-- i)) (exp i (ord (S O) i))) (rewrite-r lzero lzero nat m (λ (X-- : nat) -> eq lzero nat (exp i (ord m i)) (exp i (ord X-- i))) (refl lzero nat (exp i (ord m i))) (S O) Hm) (S O) Hm)) (S O) (bigop-false (S n) nat (S O) times (λ (p : nat) -> exp p (ord (S O) p)))) m Hm) (le-to-or-lt-eq (S O) m posm)) (true-or-false (andb (primeb n) (dividesb n m)))) q
pi-p-primeb-dividesb : (n : nat) -> (X-- : lt O n) -> eq lzero nat n (bigop (S n) (λ (p : nat) -> andb (primeb p) (dividesb p n)) nat (S O) times (λ (p : nat) -> exp p (ord n p)))
pi-p-primeb-dividesb = λ (n : nat) -> λ (posn : lt O n) -> lt-max-to-pi-p-primeb (S n) n posn (lt-max-n (λ (i : nat) -> andb (primeb i) (dividesb i n)) (S n) (le-S (S O) n posn))
pi-p-primeb : (n : nat) -> (X-- : lt O n) -> eq lzero nat n (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (ord n p)))
pi-p-primeb = λ (n : nat) -> λ (posn : lt O n) -> eq-ind lzero lzero nat (bigop (S n) (λ (p : nat) -> andb (primeb p) (dividesb p n)) nat (S O) times (λ (p : nat) -> exp p (ord n p))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bigop (S n) (λ (p : nat) -> andb (primeb p) (dividesb p n)) nat (S O) times (λ (p : nat) -> exp p (ord n p))) x-1) -> eq lzero nat n x-1) (pi-p-primeb-dividesb n posn) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (ord n p))) (eq-pi-p-primeb-divides-b (S n) n)
le-ord-log : (n : nat) -> (p : nat) -> (X-- : lt O n) -> (X--1 : lt (S O) p) -> le (ord n p) (log p n)
le-ord-log = λ (n : nat) -> λ (p : nat) -> λ (posn : lt O n) -> λ (lt1p : lt (S O) p) -> eq-ind-r lzero lzero nat (times (exp p (ord n p)) (ord-rem n p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p (ord n p)) (ord-rem n p))) -> le (ord n p) (log p x)) (eq-ind-r lzero lzero nat (plus (ord n p) (log p (ord-rem n p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (ord n p) (log p (ord-rem n p)))) -> le (ord n p) x) (le-plus-n-r (log p (ord-rem n p)) (ord n p)) (log p (times (exp p (ord n p)) (ord-rem n p))) (log-exp p (ord n p) (ord-rem n p) lt1p (lt-O-ord-rem p n lt1p posn))) n (exp-ord p n lt1p posn)
sigma-p-dividesb : (m : nat) -> (n : nat) -> (p : nat) -> (X-- : lt O n) -> (X--1 : prime p) -> (X--2 : Not lzero (divides p n)) -> eq lzero nat m (bigop m (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p m) n)) nat O plus (λ (i : nat) -> S O))
sigma-p-dividesb = λ (m : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (n : nat) -> (p : nat) -> (X-- : lt O n) -> (X--1 : prime p) -> (X--2 : Not lzero (divides p n)) -> eq lzero nat X-x-365 (bigop X-x-365 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p X-x-365) n)) nat O plus (λ (i : nat) -> S O))) (λ (n : nat) -> λ (p : nat) -> λ (auto : lt O n) -> λ (auto' : prime p) -> λ (auto'' : Not lzero (divides p n)) -> refl lzero nat O) (λ (m0 : nat) -> λ (Hind : (n : nat) -> (p : nat) -> (X-- : lt O n) -> (X--1 : prime p) -> (X--2 : Not lzero (divides p n)) -> eq lzero nat m0 (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p m0) n)) nat O plus (λ (i : nat) -> S O))) -> λ (n : nat) -> λ (p : nat) -> λ (posn : lt O n) -> λ (primep : prime p) -> λ (ndivp : Not lzero (divides p n)) -> eq-ind-r lzero lzero nat (plus (S O) (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S O) (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)))) -> eq lzero nat (S m0) x) (eq-ind-r lzero lzero nat (plus (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)) (S O))) -> eq lzero nat (S m0) x) (eq-ind lzero lzero nat (S (plus (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)) O)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (plus (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)) O)) x-1) -> eq lzero nat (S m0) x-1) (eq-f lzero lzero nat nat S m0 (plus (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)) O) (eq-ind lzero lzero nat (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)) x-1) -> eq lzero nat m0 x-1) (eq-ind-r lzero lzero nat (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p m0) n)) nat O plus (λ (i : nat) -> S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p m0) n)) nat O plus (λ (i : nat) -> S O))) -> eq lzero nat x (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O))) (same-bigop m0 (λ (X-- : nat) -> dividesb (exp p (S X--)) (times (exp p m0) n)) (λ (X-- : nat) -> dividesb (exp p (S X--)) (times (exp p (S m0)) n)) nat O plus (λ (X-- : nat) -> S O) (λ (X-- : nat) -> S O) (λ (i : nat) -> λ (ltim : lt i m0) -> match-Or lzero lzero (eq lzero bool (dividesb (exp p (S i)) (times (exp p m0) n)) true) (eq lzero bool (dividesb (exp p (S i)) (times (exp p m0) n)) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (dividesb (exp p (S i)) (times (exp p m0) n)) true) (eq lzero bool (dividesb (exp p (S i)) (times (exp p m0) n)) false)) -> eq lzero bool (dividesb (exp p (S i)) (times (exp p m0) n)) (dividesb (exp p (S i)) (times (exp p (S m0)) n))) (λ (Hc : eq lzero bool (dividesb (exp p (S i)) (times (exp p m0) n)) true) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero bool x (dividesb (exp p (S i)) (times (exp p (S m0)) n))) (sym-eq lzero bool (dividesb (exp p (S i)) (times (exp p (S m0)) n)) true (divides-to-dividesb-true (exp p (S i)) (times (exp p (S m0)) n) (lt-O-exp p (S i) (prime-to-lt-O p primep)) (quotient (exp p (S i)) (times (exp p (S m0)) n) (times (exp p (minus m0 i)) n) (eq-ind lzero lzero nat (times (times (exp p (S i)) (exp p (minus m0 i))) n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (exp p (S i)) (exp p (minus m0 i))) n) x-1) -> eq lzero nat (times (exp p (S m0)) n) x-1) (eq-ind lzero lzero nat (exp p (plus (S i) (minus m0 i))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp p (plus (S i) (minus m0 i))) x-1) -> eq lzero nat (times (exp p (S m0)) n) (times x-1 n)) (eq-f2 lzero lzero lzero nat nat nat times (exp p (S m0)) (exp p (plus (S i) (minus m0 i))) n n (eq-f lzero lzero nat nat (exp p) (S m0) (plus (S i) (minus m0 i)) (eq-f lzero lzero nat nat S m0 (plus i (minus m0 i)) (eq-ind-r lzero lzero nat (plus (minus m0 i) i) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (minus m0 i) i)) -> eq lzero nat m0 x) (plus-minus-m-m m0 i (lt-to-le i m0 ltim)) (plus i (minus m0 i)) (commutative-plus i (minus m0 i))))) (refl lzero nat n)) (times (exp p (S i)) (exp p (minus m0 i))) (exp-plus-times p (S i) (minus m0 i))) (times (exp p (S i)) (times (exp p (minus m0 i)) n)) (associative-times (exp p (S i)) (exp p (minus m0 i)) n))))) (dividesb (exp p (S i)) (times (exp p m0) n)) Hc) (λ (Hc : eq lzero bool (dividesb (exp p (S i)) (times (exp p m0) n)) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool x (dividesb (exp p (S i)) (times (exp p (S m0)) n))) (False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero bool false (dividesb (exp p (S i)) (times (exp p (S m0)) n))) (absurd lzero (divides (exp p (S i)) (times (exp p m0) n)) (quotient (exp p (S i)) (times (exp p m0) n) (times (exp p (minus m0 (S i))) n) (eq-ind lzero lzero nat (times (times (exp p (S i)) (exp p (minus m0 (S i)))) n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (exp p (S i)) (exp p (minus m0 (S i)))) n) x-1) -> eq lzero nat (times (exp p m0) n) x-1) (eq-ind lzero lzero nat (exp p (plus (S i) (minus m0 (S i)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp p (plus (S i) (minus m0 (S i)))) x-1) -> eq lzero nat (times (exp p m0) n) (times x-1 n)) (eq-f2 lzero lzero lzero nat nat nat times (exp p m0) (exp p (plus (S i) (minus m0 (S i)))) n n (eq-f lzero lzero nat nat (exp p) m0 (plus (S i) (minus m0 (S i))) (eq-ind-r lzero lzero nat (plus (minus m0 (S i)) (S i)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (minus m0 (S i)) (S i))) -> eq lzero nat m0 x) (plus-minus-m-m m0 (S i) ltim) (plus (S i) (minus m0 (S i))) (commutative-plus (S i) (minus m0 (S i))))) (refl lzero nat n)) (times (exp p (S i)) (exp p (minus m0 (S i)))) (exp-plus-times p (S i) (minus m0 (S i)))) (times (exp p (S i)) (times (exp p (minus m0 (S i))) n)) (associative-times (exp p (S i)) (exp p (minus m0 (S i))) n))) (dividesb-false-to-not-divides (exp p (S i)) (times (exp p m0) n) Hc))) (dividesb (exp p (S i)) (times (exp p m0) n)) Hc) (true-or-false (dividesb (exp p (S i)) (times (exp p m0) n)))) (λ (i : nat) -> λ (auto : lt i m0) -> λ (auto' : eq lzero bool (dividesb (exp p (S i)) (times (exp p m0) n)) true) -> refl lzero nat (S O))) m0 (Hind n p posn primep ndivp)) (plus (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)) O) (plus-n-O (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O))))) (plus (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)) (S O)) (plus-n-Sm (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)) O)) (plus (S O) (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O))) (commutative-plus (S O) (bigop m0 (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)))) (bigop (S m0) (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p (S m0)) n)) nat O plus (λ (i : nat) -> S O)) (bigop-Strue m0 (λ (X-- : nat) -> dividesb (exp p (S X--)) (times (exp p (S m0)) n)) nat O plus (λ (X-- : nat) -> S O) (divides-to-dividesb-true (exp p (S m0)) (times (exp p (S m0)) n) (lt-O-exp p (S m0) (prime-to-lt-O p primep)) (quotient (exp p (S m0)) (times (exp p (S m0)) n) n (rewrite-r lzero lzero nat (times n (exp p (S m0))) (λ (X-- : nat) -> eq lzero nat X-- (times (exp p (S m0)) n)) (rewrite-r lzero lzero nat (times n (exp p (S m0))) (λ (X-- : nat) -> eq lzero nat (times n (exp p (S m0))) X--) (refl lzero nat (times n (exp p (S m0)))) (times (exp p (S m0)) n) (commutative-times (exp p (S m0)) n)) (times (exp p (S m0)) n) (commutative-times (exp p (S m0)) n)))))) m
sigma-p-dividesb1 : (m : nat) -> (n : nat) -> (p : nat) -> (k : nat) -> (X-- : lt O n) -> (X--1 : prime p) -> (X--2 : Not lzero (divides p n)) -> (X--3 : le m k) -> eq lzero nat m (bigop k (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p m) n)) nat O plus (λ (i : nat) -> S O))
sigma-p-dividesb1 = λ (m : nat) -> λ (n : nat) -> λ (p : nat) -> λ (k : nat) -> λ (posn : lt O n) -> λ (primep : prime p) -> λ (ndivp : Not lzero (divides p n)) -> λ (lemk : le m k) -> eq-ind-r lzero lzero nat (bigop m (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p m) n)) nat O plus (λ (i : nat) -> S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop m (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p m) n)) nat O plus (λ (i : nat) -> S O))) -> eq lzero nat x (bigop k (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p m) n)) nat O plus (λ (i : nat) -> S O))) (eq-ind-r lzero lzero nat (bigop k (λ (i : nat) -> match-bool lzero (λ (X-0 : bool) -> bool) false (dividesb (exp p (S i)) (times (exp p m) n)) (leb m i)) nat O plus (λ (i : nat) -> S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop k (λ (i : nat) -> match-bool lzero (λ (X-0 : bool) -> bool) false (dividesb (exp p (S i)) (times (exp p m) n)) (leb m i)) nat O plus (λ (i : nat) -> S O))) -> eq lzero nat x (bigop k (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p m) n)) nat O plus (λ (i : nat) -> S O))) (same-bigop k (λ (X-- : nat) -> match-bool lzero (λ (X-0 : bool) -> bool) false (dividesb (exp p (S X--)) (times (exp p m) n)) (leb m X--)) (λ (X-- : nat) -> dividesb (exp p (S X--)) (times (exp p m) n)) nat O plus (λ (X-- : nat) -> S O) (λ (X-- : nat) -> S O) (λ (i : nat) -> λ (ltik : lt i k) -> match-Or lzero lzero (eq lzero bool (leb m i) true) (eq lzero bool (leb m i) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (leb m i) true) (eq lzero bool (leb m i) false)) -> eq lzero bool (match-bool lzero (λ (X-0 : bool) -> bool) false (dividesb (exp p (S i)) (times (exp p m) n)) (leb m i)) (dividesb (exp p (S i)) (times (exp p m) n))) (λ (Him : eq lzero bool (leb m i) true) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero bool (match-bool lzero (λ (X-0 : bool) -> bool) false (dividesb (exp p (S i)) (times (exp p m) n)) x) (dividesb (exp p (S i)) (times (exp p m) n))) (sym-eq lzero bool (dividesb (exp p (S i)) (times (exp p m) n)) false (not-divides-to-dividesb-false (exp p (S i)) (times (exp p m) n) (lt-O-exp p (S i) (prime-to-lt-O p primep)) (nmk lzero (divides (exp p (S i)) (times (exp p m) n)) (λ (Hdiv : divides (exp p (S i)) (times (exp p m) n)) -> absurd lzero (lt i m) (eq-ind-r lzero lzero nat (plus m O) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus m O)) -> lt i x) (eq-ind lzero lzero nat (ord n p) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (ord n p) x-1) -> lt i (plus m x-1)) (eq-ind lzero lzero nat (ord (exp p m) p) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (ord (exp p m) p) x-1) -> lt i (plus x-1 (ord n p))) (eq-ind lzero lzero nat (ord (times (exp p m) n) p) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (ord (times (exp p m) n) p) x-1) -> lt i x-1) (eq-ind lzero lzero nat (ord (exp p (S i)) p) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (ord (exp p (S i)) p) x-1) -> le x-1 (ord (times (exp p m) n) p)) (divides-to-le-ord p (exp p (S i)) (times (exp p m) n) (lt-O-exp p (S i) (prime-to-lt-O p primep)) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> lt x (times (exp p m) n)) (lt-times O (exp p m) O n (lt-O-exp p m (prime-to-lt-O p primep)) posn) O (times-n-O O)) primep Hdiv) (S i) (ord-exp p (S i) (prime-to-lt-SO p primep))) (plus (ord (exp p m) p) (ord n p)) (ord-times p (exp p m) n (lt-O-exp p m (prime-to-lt-O p primep)) posn primep)) m (ord-exp p m (prime-to-lt-SO p primep))) O (not-divides-to-ord-O p n primep ndivp)) m (plus-n-O m)) (le-to-not-lt m i (leb-true-to-le m i Him)))))) (leb m i) Him) (λ (Him : eq lzero bool (leb m i) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool (match-bool lzero (λ (X-0 : bool) -> bool) false (dividesb (exp p (S i)) (times (exp p m) n)) x) (dividesb (exp p (S i)) (times (exp p m) n))) (refl lzero bool (match-bool lzero (λ (X-0 : bool) -> bool) false (dividesb (exp p (S i)) (times (exp p m) n)) false)) (leb m i) Him) (true-or-false (leb m i))) (λ (i : nat) -> λ (auto : lt i k) -> λ (auto' : eq lzero bool (match-bool lzero (λ (X-0 : bool) -> bool) false (dividesb (exp p (S i)) (times (exp p m) n)) (leb m i)) true) -> refl lzero nat (S O))) (bigop m (λ (i : nat) -> dividesb (exp p (S i)) (times (exp p m) n)) nat O plus (λ (i : nat) -> S O)) (pad-bigop k m (λ (X-- : nat) -> dividesb (exp p (S X--)) (times (exp p m) n)) nat O plus (λ (X-- : nat) -> S O) lemk)) m (sigma-p-dividesb m n p posn primep ndivp)
eq-ord-sigma-p : (n : nat) -> (m : nat) -> (x : nat) -> (X-- : lt O n) -> (X--1 : prime x) -> (X--2 : le (exp x m) n) -> (X--3 : lt n (exp x (S m))) -> eq lzero nat (ord n x) (bigop m (λ (i : nat) -> dividesb (exp x (S i)) n) nat O plus (λ (i : nat) -> S O))
eq-ord-sigma-p = λ (n : nat) -> λ (m : nat) -> λ (x : nat) -> λ (posn : lt O n) -> λ (primex : prime x) -> λ (Hexp : le (exp x m) n) -> λ (ltn : lt n (exp x (S m))) -> eq-ind-r lzero lzero nat (times (exp x (ord n x)) (ord-rem n x)) (λ (x0 : nat) -> λ (X-- : eq lzero nat x0 (times (exp x (ord n x)) (ord-rem n x))) -> eq lzero nat (ord n x) (bigop m (λ (i : nat) -> dividesb (exp x (S i)) x0) nat O plus (λ (i : nat) -> S O))) (sigma-p-dividesb1 (ord n x) (ord-rem n x) x m (lt-O-ord-rem x n (prime-to-lt-SO x primex) posn) primex (not-divides-ord-rem n x posn (prime-to-lt-SO x primex)) (le-S-S-to-le (ord n x) m (le-to-lt-to-lt (ord n x) (log x n) (S m) (le-ord-log n x posn (prime-to-lt-SO x primex)) (lt-exp-to-lt x (log x n) (S m) (lt-to-le (S O) x (prime-to-lt-SO x primex)) (le-to-lt-to-lt (exp x (log x n)) n (exp x (S m)) (le-exp-log x n posn) ltn))))) n (exp-ord x n (prime-to-lt-SO x primex) posn)
pi-p-primeb1 : (n : nat) -> (X-- : lt O n) -> eq lzero nat n (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> dividesb (exp p (S i)) n) nat (S O) times (λ (i : nat) -> p)))
pi-p-primeb1 = λ (n : nat) -> λ (posn : lt O n) -> eq-ind-r lzero lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (ord n p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (ord n p)))) -> eq lzero nat x (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> dividesb (exp p (S i)) n) nat (S O) times (λ (i : nat) -> p)))) (same-bigop (S n) primeb primeb nat (S O) times (λ (X-- : nat) -> exp X-- (ord n X--)) (λ (X-- : nat) -> bigop (log X-- n) (λ (i : nat) -> dividesb (exp X-- (S i)) n) nat (S O) times (λ (i : nat) -> X--)) (λ (i : nat) -> λ (auto : lt i (S n)) -> refl lzero bool (primeb i)) (λ (p : nat) -> λ (ltp : lt p (S n)) -> λ (primep : eq lzero bool (primeb p) true) -> eq-ind-r lzero lzero nat (exp p (bigop (log p n) (λ (i : nat) -> dividesb (exp p (S i)) n) nat O plus (λ (i : nat) -> S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (exp p (bigop (log p n) (λ (i : nat) -> dividesb (exp p (S i)) n) nat O plus (λ (i : nat) -> S O)))) -> eq lzero nat (exp p (ord n p)) x) (eq-f lzero lzero nat nat (exp p) (ord n p) (bigop (log p n) (λ (i : nat) -> dividesb (exp p (S i)) n) nat O plus (λ (i : nat) -> S O)) (eq-ord-sigma-p n (log p n) p posn (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb p) primep)) (le-exp-log p n posn) (lt-exp-log p n (prime-to-lt-SO p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb p) primep)))))) (bigop (log p n) (λ (i : nat) -> dividesb (exp p (S i)) n) nat (S O) times (λ (i : nat) -> p)) (exp-sigma (log p n) p (λ (X-- : nat) -> dividesb (exp p (S X--)) n)))) n (pi-p-primeb n posn)
eq-fact-pi-p : (n : nat) -> eq lzero nat (fact n) (bigop (S n) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i))
eq-fact-pi-p = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat (fact X-x-365) (bigop (S X-x-365) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i))) (refl lzero nat (fact O)) (λ (n1 : nat) -> λ (Hind : eq lzero nat (fact n1) (bigop (S n1) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i))) -> eq-ind-r lzero lzero nat (times (S n1) (fact n1)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S n1) (fact n1))) -> eq lzero nat x (bigop (S (S n1)) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i))) (eq-ind-r lzero lzero nat (times (S n1) (bigop (S n1) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S n1) (bigop (S n1) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i)))) -> eq lzero nat (times (S n1) (fact n1)) x) (eq-f lzero lzero nat nat (times (S n1)) (fact n1) (bigop (S n1) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i)) (rewrite-l lzero lzero nat (fact n1) (λ (X-- : nat) -> eq lzero nat (fact n1) X--) (refl lzero nat (fact n1)) (bigop (S n1) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i)) Hind)) (bigop (S (S n1)) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i)) (bigop-Strue (S n1) (leb (S O)) nat (S O) times (λ (X-- : nat) -> X--) (refl lzero bool (leb (S O) (S n1))))) (times (fact n1) (S n1)) (commutative-times (fact n1) (S n1))) n
let-clause-1648 : (n : nat) -> (q : nat) -> (posq : lt O q) -> (n1 : nat) -> (Hind : eq lzero nat n1 (plus (times (bigop (S n1) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) (mod n1 q))) -> (X-clearme : And lzero lzero (divides q (S n1)) (eq lzero nat (S n1) (times (S (div n1 q)) q))) -> (divq : divides q (S n1)) -> (eqn1 : eq lzero nat (S n1) (times (S (div n1 q)) q)) -> eq lzero nat (S n1) (plus q (times q (div n1 q)))
let-clause-1648 = λ (n : nat) -> λ (q : nat) -> λ (posq : lt O q) -> λ (n1 : nat) -> λ (Hind : eq lzero nat n1 (plus (times (bigop (S n1) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) (mod n1 q))) -> λ (X-clearme : And lzero lzero (divides q (S n1)) (eq lzero nat (S n1) (times (S (div n1 q)) q))) -> λ (divq : divides q (S n1)) -> λ (eqn1 : eq lzero nat (S n1) (times (S (div n1 q)) q)) -> rewrite-r lzero lzero nat (times q (S (div n1 q))) (λ (X-- : nat) -> eq lzero nat (S n1) X--) (rewrite-l lzero lzero nat (times (S (div n1 q)) q) (λ (X-- : nat) -> eq lzero nat (S n1) X--) eqn1 (times q (S (div n1 q))) (commutative-times (S (div n1 q)) q)) (plus q (times q (div n1 q))) (times-n-Sm q (div n1 q))
eq-sigma-p-div : (n : nat) -> (q : nat) -> (X-- : lt O q) -> eq lzero nat (bigop (S n) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) (div n q)
eq-sigma-p-div = λ (n : nat) -> λ (q : nat) -> λ (posq : lt O q) -> div-mod-spec-to-eq n q (bigop (S n) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) (mod n q) (div n q) (mod n q) (div-mod-spec-intro n q (bigop (S n) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) (mod n q) (lt-mod-m-m n q posq) (nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat X-x-365 (plus (times (bigop (S X-x-365) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) (mod X-x-365 q))) (match-nat lzero (λ (X-- : nat) -> eq lzero nat O (match-nat lzero (λ (X-0 : nat) -> nat) O (λ (p : nat) -> O) X--)) (refl lzero nat O) (λ (auto : nat) -> refl lzero nat O) q) (λ (n1 : nat) -> λ (Hind : eq lzero nat n1 (plus (times (bigop (S n1) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) (mod n1 q))) -> match-Or lzero lzero (And lzero lzero (divides q (S n1)) (eq lzero nat (S n1) (times (S (div n1 q)) q))) (And lzero lzero (Not lzero (divides q (S n1))) (eq lzero nat (S n1) (plus (times (div n1 q) q) (S (mod n1 q))))) lzero (λ (X-- : Or lzero lzero (And lzero lzero (divides q (S n1)) (eq lzero nat (S n1) (times (S (div n1 q)) q))) (And lzero lzero (Not lzero (divides q (S n1))) (eq lzero nat (S n1) (plus (times (div n1 q) q) (S (mod n1 q)))))) -> eq lzero nat (S n1) (plus (times (bigop (S (S n1)) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) (mod (S n1) q))) (λ (X-clearme : And lzero lzero (divides q (S n1)) (eq lzero nat (S n1) (times (S (div n1 q)) q))) -> match-And lzero lzero (divides q (S n1)) (eq lzero nat (S n1) (times (S (div n1 q)) q)) lzero (λ (X-- : And lzero lzero (divides q (S n1)) (eq lzero nat (S n1) (times (S (div n1 q)) q))) -> eq lzero nat (S n1) (plus (times (bigop (S (S n1)) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) (mod (S n1) q))) (λ (divq : divides q (S n1)) -> λ (eqn1 : eq lzero nat (S n1) (times (S (div n1 q)) q)) -> eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (S n1) (plus (times (bigop (S (S n1)) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) x)) (eq-ind lzero lzero nat (times (bigop (S (S n1)) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (bigop (S (S n1)) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) x-1) -> eq lzero nat (S n1) x-1) (eq-ind-r lzero lzero nat (plus (S O) (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S O) (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)))) -> eq lzero nat (S n1) (times x q)) (eq-ind-r lzero lzero nat (times (S (div n1 q)) q) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (div n1 q)) q)) -> eq lzero nat x (times (plus (S O) (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O))) q)) (eq-f2 lzero lzero lzero nat nat nat times (S (div n1 q)) (plus (S O) (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O))) q q (eq-ind lzero lzero nat (plus (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) (S O)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) (S O)) x-1) -> eq lzero nat (S (div n1 q)) x-1) (eq-ind lzero lzero nat (S (plus (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) O)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (plus (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) O)) x-1) -> eq lzero nat (S (div n1 q)) x-1) (eq-ind lzero lzero nat (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) x-1) -> eq lzero nat (S (div n1 q)) (S x-1)) (eq-f lzero lzero nat nat S (div n1 q) (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) (div-mod-spec-to-eq n1 q (div n1 q) (mod n1 q) (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) (mod n1 q) (div-mod-spec-div-mod n1 q posq) (div-mod-spec-intro n1 q (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) (mod n1 q) (lt-mod-m-m n1 q posq) (rewrite-r lzero lzero nat (plus q (times q (div n1 q))) (λ (X-- : nat) -> eq lzero nat n1 (plus (times (bigop X-- (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) q) (mod n1 q))) (rewrite-r lzero lzero nat (times q (bigop (plus q (times q (div n1 q))) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O))) (λ (X-- : nat) -> eq lzero nat n1 (plus X-- (mod n1 q))) (rewrite-r lzero lzero nat (plus (mod n1 q) (times q (bigop (plus q (times q (div n1 q))) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)))) (λ (X-- : nat) -> eq lzero nat n1 X--) (rewrite-l lzero lzero nat n1 (λ (X-- : nat) -> eq lzero nat n1 X--) (refl lzero nat n1) (plus (mod n1 q) (times q (bigop (plus q (times q (div n1 q))) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)))) (rewrite-l lzero lzero nat (plus (times q (bigop (plus q (times q (div n1 q))) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O))) (mod n1 q)) (λ (X-- : nat) -> eq lzero nat n1 X--) (rewrite-l lzero lzero nat (times (bigop (plus q (times q (div n1 q))) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) (λ (X-- : nat) -> eq lzero nat n1 (plus X-- (mod n1 q))) (rewrite-l lzero lzero nat (S n1) (λ (X-- : nat) -> eq lzero nat n1 (plus (times (bigop X-- (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) (mod n1 q))) Hind (plus q (times q (div n1 q))) (let-clause-1648 n q posq n1 Hind X-clearme divq eqn1)) (times q (bigop (plus q (times q (div n1 q))) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O))) (commutative-times (bigop (plus q (times q (div n1 q))) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q)) (plus (mod n1 q) (times q (bigop (plus q (times q (div n1 q))) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)))) (commutative-plus (times q (bigop (plus q (times q (div n1 q))) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O))) (mod n1 q)))) (plus (times q (bigop (plus q (times q (div n1 q))) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O))) (mod n1 q)) (commutative-plus (times q (bigop (plus q (times q (div n1 q))) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O))) (mod n1 q))) (times (bigop (plus q (times q (div n1 q))) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) q) (commutative-times (bigop (plus q (times q (div n1 q))) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) q)) (S n1) (let-clause-1648 n q posq n1 Hind X-clearme divq eqn1))))) (plus (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) O) (plus-n-O (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)))) (plus (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) (S O)) (plus-n-Sm (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) O)) (plus (S O) (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O))) (commutative-plus (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) (S O))) (refl lzero nat q)) (S n1) eqn1) (bigop (S (S n1)) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) (bigop-Strue (S n1) (λ (X-- : nat) -> andb (leb (S O) X--) (dividesb q X--)) nat O plus (λ (X-- : nat) -> S O) (true-to-andb-true (leb (S O) (S n1)) (dividesb q (S n1)) (refl lzero bool (leb (S O) (S n1))) (divides-to-dividesb-true q (S n1) posq divq)))) (plus (times (bigop (S (S n1)) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) O) (plus-n-O (times (bigop (S (S n1)) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q))) (mod (S n1) q) (divides-to-mod-O q (S n1) posq divq)) X-clearme) (λ (X-clearme : And lzero lzero (Not lzero (divides q (S n1))) (eq lzero nat (S n1) (plus (times (div n1 q) q) (S (mod n1 q))))) -> match-And lzero lzero (Not lzero (divides q (S n1))) (eq lzero nat (S n1) (plus (times (div n1 q) q) (S (mod n1 q)))) lzero (λ (X-- : And lzero lzero (Not lzero (divides q (S n1))) (eq lzero nat (S n1) (plus (times (div n1 q) q) (S (mod n1 q))))) -> eq lzero nat (S n1) (plus (times (bigop (S (S n1)) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) (mod (S n1) q))) (λ (ndiv : Not lzero (divides q (S n1))) -> λ (eqn1 : eq lzero nat (S n1) (plus (times (div n1 q) q) (S (mod n1 q)))) -> eq-ind-r lzero lzero nat (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O))) -> eq lzero nat (S n1) (plus (times x q) (mod (S n1) q))) (eq-ind-r lzero lzero nat (S (mod n1 q)) (λ (x : nat) -> λ (X-- : eq lzero nat x (S (mod n1 q))) -> eq lzero nat (S n1) (plus (times (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) q) x)) (eq-ind lzero lzero nat (S (plus (times (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) q) (mod n1 q))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (plus (times (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) q) (mod n1 q))) x-1) -> eq lzero nat (S n1) x-1) (eq-f lzero lzero nat nat S n1 (plus (times (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) q) (mod n1 q)) (rewrite-r lzero lzero nat (times q (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O))) (λ (X-- : nat) -> eq lzero nat n1 (plus X-- (mod n1 q))) (rewrite-r lzero lzero nat (plus (mod n1 q) (times q (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)))) (λ (X-- : nat) -> eq lzero nat n1 X--) (rewrite-l lzero lzero nat n1 (λ (X-- : nat) -> eq lzero nat n1 X--) (refl lzero nat n1) (plus (mod n1 q) (times q (bigop (S n1) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)))) (rewrite-l lzero lzero nat (plus (times q (bigop (S n1) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O))) (mod n1 q)) (λ (X-- : nat) -> eq lzero nat n1 X--) (rewrite-l lzero lzero nat (times (bigop (S n1) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q) (λ (X-- : nat) -> eq lzero nat n1 (plus X-- (mod n1 q))) Hind (times q (bigop (S n1) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O))) (commutative-times (bigop (S n1) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)) q)) (plus (mod n1 q) (times q (bigop (S n1) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O)))) (commutative-plus (times q (bigop (S n1) (λ (m : nat) -> andb (leb (S O) m) (dividesb q m)) nat O plus (λ (m : nat) -> S O))) (mod n1 q)))) (plus (times q (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O))) (mod n1 q)) (commutative-plus (times q (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O))) (mod n1 q))) (times (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) q) (commutative-times (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) q))) (plus (times (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) q) (S (mod n1 q))) (plus-n-Sm (times (bigop (S n1) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) q) (mod n1 q))) (mod (S n1) q) (mod-S n1 q posq (match-Or lzero lzero (lt (S (mod n1 q)) q) (eq lzero nat (S (mod n1 q)) q) lzero (λ (X-- : Or lzero lzero (lt (S (mod n1 q)) q) (eq lzero nat (S (mod n1 q)) q)) -> lt (S (mod n1 q)) q) (λ (auto : lt (S (mod n1 q)) q) -> auto) (λ (eqq : eq lzero nat (S (mod n1 q)) q) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt (S (mod n1 q)) q) (match-Not lzero (divides q (S n1)) lzero (λ (X-- : Not lzero (divides q (S n1))) -> False lzero) (λ (Hdiv : (X-- : divides q (S n1)) -> False lzero) -> Hdiv (quotient q (S n1) (S (div n1 q)) (eq-ind lzero lzero nat (plus q (times q (div n1 q))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus q (times q (div n1 q))) x-1) -> eq lzero nat (S n1) x-1) (eq-ind lzero lzero nat (plus (times q (div n1 q)) q) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (times q (div n1 q)) q) x-1) -> eq lzero nat (S n1) x-1) (rewrite-r lzero lzero nat (plus q (times q (div n1 q))) (λ (X-- : nat) -> eq lzero nat X-- (plus (times q (div n1 q)) q)) (rewrite-r lzero lzero nat (plus q (times q (div n1 q))) (λ (X-- : nat) -> eq lzero nat (plus q (times q (div n1 q))) X--) (refl lzero nat (plus q (times q (div n1 q)))) (plus (times q (div n1 q)) q) (commutative-plus (times q (div n1 q)) q)) (S n1) (rewrite-l lzero lzero nat (plus (times q (div n1 q)) q) (λ (X-- : nat) -> eq lzero nat (S n1) X--) (rewrite-l lzero lzero nat (S (mod n1 q)) (λ (X-- : nat) -> eq lzero nat (S n1) (plus (times q (div n1 q)) X--)) (rewrite-l lzero lzero nat (times (div n1 q) q) (λ (X-- : nat) -> eq lzero nat (S n1) (plus X-- (S (mod n1 q)))) eqn1 (times q (div n1 q)) (commutative-times (div n1 q) q)) q eqq) (plus q (times q (div n1 q))) (commutative-plus (times q (div n1 q)) q))) (plus q (times q (div n1 q))) (commutative-plus (times q (div n1 q)) q)) (times q (S (div n1 q))) (times-n-Sm q (div n1 q))))) ndiv)) (le-to-or-lt-eq (S (mod n1 q)) q (lt-mod-m-m n1 q posq))))) (bigop (S (S n1)) (λ (i : nat) -> andb (leb (S O) i) (dividesb q i)) nat O plus (λ (i : nat) -> S O)) (bigop-Sfalse (S n1) (λ (X-- : nat) -> andb (leb (S O) X--) (dividesb q X--)) nat O plus (λ (X-- : nat) -> S O) (eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool (andb (leb (S O) (S n1)) x) false) (refl lzero bool (andb (leb (S O) (S n1)) false)) (dividesb q (S n1)) (not-divides-to-dividesb-false q (S n1) posq ndiv)))) X-clearme) (or-div-mod1 n1 q posq)) n)) (div-mod-spec-div-mod n q posq)
timesACdef : (n : nat) -> (m : nat) -> eq lzero nat (aop--o--op lzero nat (S O) timesAC n m) (times n m)
timesACdef = λ (n : nat) -> λ (m : nat) -> refl lzero nat (aop--o--op lzero nat (S O) timesAC n m)
fact-pi-p : (n : nat) -> eq lzero nat (fact n) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div n (exp p (S i))))))
fact-pi-p = λ (n : nat) -> eq-ind-r lzero lzero nat (bigop (S n) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i))) -> eq lzero nat x (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div n (exp p (S i))))))) (trans-eq lzero nat (bigop (S n) (λ (i : nat) -> leb (S O) i) nat (S O) times (λ (i : nat) -> i)) (bigop (S n) (λ (m : nat) -> leb (S O) m) nat (S O) times (λ (m : nat) -> bigop (S m) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p m) (λ (i : nat) -> dividesb (exp p (S i)) m) nat (S O) times (λ (i : nat) -> p)))) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div n (exp p (S i)))))) (same-bigop (S n) (leb (S O)) (leb (S O)) nat (S O) times (λ (X-- : nat) -> X--) (λ (X-- : nat) -> bigop (S X--) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p X--) (λ (i : nat) -> dividesb (exp p (S i)) X--) nat (S O) times (λ (i : nat) -> p))) (λ (i : nat) -> λ (auto : lt i (S n)) -> refl lzero bool (leb (S O) i)) (λ (x : nat) -> λ (Hx1 : lt x (S n)) -> λ (Hx2 : eq lzero bool (leb (S O) x) true) -> pi-p-primeb1 x (leb-true-to-le (S O) x (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (leb (S O) x) Hx2)))) (trans-eq lzero nat (bigop (S n) (λ (m : nat) -> leb (S O) m) nat (S O) times (λ (m : nat) -> bigop (S m) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p m) (λ (i : nat) -> dividesb (exp p (S i)) m) nat (S O) times (λ (i : nat) -> p)))) (bigop (S n) (λ (m : nat) -> leb (S O) m) nat (S O) times (λ (m : nat) -> bigop (S m) (λ (p : nat) -> andb (primeb p) (leb p m)) nat (S O) times (λ (p : nat) -> bigop (log p m) (λ (i : nat) -> dividesb (exp p (S i)) m) nat (S O) times (λ (i : nat) -> p)))) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div n (exp p (S i)))))) (same-bigop (S n) (leb (S O)) (leb (S O)) nat (S O) times (λ (X-- : nat) -> bigop (S X--) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p X--) (λ (i : nat) -> dividesb (exp p (S i)) X--) nat (S O) times (λ (i : nat) -> p))) (λ (X-- : nat) -> bigop (S X--) (λ (p : nat) -> andb (primeb p) (leb p X--)) nat (S O) times (λ (p : nat) -> bigop (log p X--) (λ (i : nat) -> dividesb (exp p (S i)) X--) nat (S O) times (λ (i : nat) -> p))) (λ (i : nat) -> λ (auto : lt i (S n)) -> refl lzero bool (leb (S O) i)) (λ (x : nat) -> λ (Hx1 : lt x (S n)) -> λ (Hx2 : eq lzero bool (leb (S O) x) true) -> same-bigop (S x) primeb (λ (X-- : nat) -> andb (primeb X--) (leb X-- x)) nat (S O) times (λ (X-- : nat) -> bigop (log X-- x) (λ (i : nat) -> dividesb (exp X-- (S i)) x) nat (S O) times (λ (i : nat) -> X--)) (λ (X-- : nat) -> bigop (log X-- x) (λ (i : nat) -> dividesb (exp X-- (S i)) x) nat (S O) times (λ (i : nat) -> X--)) (λ (p : nat) -> λ (ltp : lt p (S x)) -> eq-ind-r lzero lzero bool true (λ (x0 : bool) -> λ (X-- : eq lzero bool x0 true) -> eq lzero bool (primeb p) (andb (primeb p) x0)) (match-bool lzero (λ (X-- : bool) -> eq lzero bool X-- (andb X-- true)) (refl lzero bool true) (refl lzero bool false) (primeb p)) (leb p x) (le-to-leb-true p x (le-S-S-to-le p x ltp))) (λ (i : nat) -> λ (auto : lt i (S x)) -> λ (auto' : eq lzero bool (primeb i) true) -> refl lzero nat (bigop (log i x) (λ (i0 : nat) -> dividesb (exp i (S i0)) x) nat (S O) times (λ (i0 : nat) -> i))))) (trans-eq lzero nat (bigop (S n) (λ (m : nat) -> leb (S O) m) nat (S O) times (λ (m : nat) -> bigop (S m) (λ (p : nat) -> andb (primeb p) (leb p m)) nat (S O) times (λ (p : nat) -> bigop (log p m) (λ (i : nat) -> dividesb (exp p (S i)) m) nat (S O) times (λ (i : nat) -> p)))) (bigop (S n) (λ (m : nat) -> leb (S O) m) nat (S O) times (λ (m : nat) -> bigop (S n) (λ (p : nat) -> andb (primeb p) (leb p m)) nat (S O) times (λ (p : nat) -> bigop (log p m) (λ (i : nat) -> dividesb (exp p (S i)) m) nat (S O) times (λ (i : nat) -> p)))) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div n (exp p (S i)))))) (same-bigop (S n) (leb (S O)) (leb (S O)) nat (S O) times (λ (X-- : nat) -> bigop (S X--) (λ (p : nat) -> andb (primeb p) (leb p X--)) nat (S O) times (λ (p : nat) -> bigop (log p X--) (λ (i : nat) -> dividesb (exp p (S i)) X--) nat (S O) times (λ (i : nat) -> p))) (λ (X-- : nat) -> bigop (S n) (λ (p : nat) -> andb (primeb p) (leb p X--)) nat (S O) times (λ (p : nat) -> bigop (log p X--) (λ (i : nat) -> dividesb (exp p (S i)) X--) nat (S O) times (λ (i : nat) -> p))) (λ (i : nat) -> λ (auto : lt i (S n)) -> refl lzero bool (leb (S O) i)) (λ (p : nat) -> λ (Hp1 : lt p (S n)) -> λ (Hp2 : eq lzero bool (leb (S O) p) true) -> pad-bigop1 (S n) (S p) (λ (X-- : nat) -> andb (primeb X--) (leb X-- p)) nat (S O) times (λ (X-- : nat) -> bigop (log X-- p) (λ (i : nat) -> dividesb (exp X-- (S i)) p) nat (S O) times (λ (i : nat) -> X--)) Hp1 (λ (i : nat) -> λ (lti : le (S p) i) -> λ (upi : lt i (S n)) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool (andb (primeb i) x) false) (match-bool lzero (λ (X-- : bool) -> eq lzero bool (andb X-- false) false) (refl lzero bool (andb true false)) (refl lzero bool (andb false false)) (primeb i)) (leb i p) (lt-to-leb-false i p lti)))) (trans-eq lzero nat (bigop (S n) (λ (m : nat) -> leb (S O) m) nat (S O) times (λ (m : nat) -> bigop (S n) (λ (p : nat) -> andb (primeb p) (leb p m)) nat (S O) times (λ (p : nat) -> bigop (log p m) (λ (i : nat) -> dividesb (exp p (S i)) m) nat (S O) times (λ (i : nat) -> p)))) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (S n) (λ (m : nat) -> leb p m) nat (S O) times (λ (m : nat) -> bigop (log p m) (λ (i : nat) -> dividesb (exp p (S i)) m) nat (S O) times (λ (i : nat) -> p)))) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div n (exp p (S i)))))) (bigop-commute (S n) (S n) (leb (S O)) (λ (X-- : nat) -> λ (X-0 : nat) -> andb (primeb X-0) (leb X-0 X--)) primeb (λ (X-- : nat) -> λ (X-0 : nat) -> leb X-0 X--) nat (S O) timesAC (λ (X-- : nat) -> λ (X-0 : nat) -> bigop (log X-0 X--) (λ (i : nat) -> dividesb (exp X-0 (S i)) X--) nat (S O) times (λ (i : nat) -> X-0)) (lt-O-S n) (lt-O-S n) (λ (i : nat) -> λ (j : nat) -> λ (lti : lt i (S n)) -> λ (ltj : lt j (S n)) -> match-Or lzero lzero (eq lzero bool (andb (primeb j) (leb j i)) true) (eq lzero bool (andb (primeb j) (leb j i)) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (andb (primeb j) (leb j i)) true) (eq lzero bool (andb (primeb j) (leb j i)) false)) -> eq lzero bool (andb (leb (S O) i) (andb (primeb j) (leb j i))) (andb (primeb j) (leb j i))) (λ (Hc : eq lzero bool (andb (primeb j) (leb j i)) true) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero bool (andb (leb (S O) i) x) x) (eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero bool (andb x true) true) (refl lzero bool (andb true true)) (leb (S O) i) (le-to-leb-true (S O) i (transitive-le (S O) j i (prime-to-lt-O j (primeb-true-to-prime j (andb-true-l (primeb j) (leb j i) Hc))) (leb-true-to-le j i (andb-true-r (primeb j) (leb j i) Hc))))) (andb (primeb j) (leb j i)) Hc) (λ (Hc : eq lzero bool (andb (primeb j) (leb j i)) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero bool (andb (leb (S O) i) x) x) (match-bool lzero (λ (X-- : bool) -> eq lzero bool (andb X-- false) false) (refl lzero bool (andb true false)) (refl lzero bool (andb false false)) (leb (S O) i)) (andb (primeb j) (leb j i)) Hc) (true-or-false (andb (primeb j) (leb j i))))) (same-bigop (S n) primeb primeb nat (S O) times (λ (X-- : nat) -> bigop (S n) (λ (m : nat) -> leb X-- m) nat (S O) times (λ (m : nat) -> bigop (log X-- m) (λ (i : nat) -> dividesb (exp X-- (S i)) m) nat (S O) times (λ (i : nat) -> X--))) (λ (X-- : nat) -> bigop (log X-- n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp X-- (div n (exp X-- (S i))))) (λ (i : nat) -> λ (auto : lt i (S n)) -> refl lzero bool (primeb i)) (λ (p : nat) -> λ (Hp1 : lt p (S n)) -> λ (Hp2 : eq lzero bool (primeb p) true) -> trans-eq lzero nat (bigop (S n) (λ (m : nat) -> leb p m) nat (S O) times (λ (m : nat) -> bigop (log p m) (λ (i : nat) -> dividesb (exp p (S i)) m) nat (S O) times (λ (i : nat) -> p))) (bigop (S n) (λ (m : nat) -> leb p m) nat (S O) times (λ (m : nat) -> bigop (log p n) (λ (i : nat) -> dividesb (exp p (S i)) m) nat (S O) times (λ (i : nat) -> p))) (bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div n (exp p (S i))))) (same-bigop (S n) (leb p) (leb p) nat (S O) times (λ (X-- : nat) -> bigop (log p X--) (λ (i : nat) -> dividesb (exp p (S i)) X--) nat (S O) times (λ (i : nat) -> p)) (λ (X-- : nat) -> bigop (log p n) (λ (i : nat) -> dividesb (exp p (S i)) X--) nat (S O) times (λ (i : nat) -> p)) (λ (i : nat) -> λ (auto : lt i (S n)) -> refl lzero bool (leb p i)) (λ (x : nat) -> λ (Hx1 : lt x (S n)) -> λ (Hx2 : eq lzero bool (leb p x) true) -> sym-eq lzero nat (bigop (log p n) (λ (i : nat) -> dividesb (exp p (S i)) x) nat (S O) times (λ (i : nat) -> p)) (bigop (log p x) (λ (i : nat) -> dividesb (exp p (S i)) x) nat (S O) times (λ (i : nat) -> p)) (sym-eq lzero nat (bigop (log p x) (λ (i : nat) -> dividesb (exp p (S i)) x) nat (S O) times (λ (i : nat) -> p)) (bigop (log p n) (λ (i : nat) -> dividesb (exp p (S i)) x) nat (S O) times (λ (i : nat) -> p)) (pad-bigop1 (log p n) (log p x) (λ (X-- : nat) -> dividesb (exp p (S X--)) x) nat (S O) times (λ (X-- : nat) -> p) (le-log p x n (prime-to-lt-SO p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb p) Hp2))) (le-S-S-to-le x n Hx1)) (λ (i : nat) -> λ (Hi1 : le (log p x) i) -> λ (Hi2 : lt i (log p n)) -> not-divides-to-dividesb-false (exp p (S i)) x (lt-O-exp p (S i) (prime-to-lt-O p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb p) Hp2)))) (not-to-not lzero (divides (exp p (S i)) x) (le (exp p (S i)) x) (λ (H : divides (exp p (S i)) x) -> divides-to-le (exp p (S i)) x (lt-to-le-to-lt O p x (prime-to-lt-O p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb p) Hp2))) (leb-true-to-le p x (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (leb p x) Hx2))) H) (lt-to-not-le x (exp p (S i)) (lt-to-le-to-lt x (exp p (S (log p x))) (exp p (S i)) (lt-exp-log p x (prime-to-lt-SO p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb p) Hp2)))) (le-exp (S (log p x)) (S i) p (prime-to-lt-O p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb p) Hp2))) (le-S-S (log p x) i Hi1)))))))))) (trans-eq lzero nat (bigop (S n) (λ (m : nat) -> leb p m) nat (S O) times (λ (m : nat) -> bigop (log p n) (λ (i : nat) -> dividesb (exp p (S i)) m) nat (S O) times (λ (i : nat) -> p))) (bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> bigop (S n) (λ (m : nat) -> andb (leb p m) (dividesb (exp p (S i)) m)) nat (S O) times (λ (m : nat) -> p))) (bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div n (exp p (S i))))) (bigop-commute (S n) (log p n) (leb p) (λ (X-- : nat) -> λ (X-0 : nat) -> dividesb (exp p (S X-0)) X--) (λ (X-- : nat) -> true) (λ (X-- : nat) -> λ (X-0 : nat) -> andb (leb p X--) (dividesb (exp p (S X-0)) X--)) nat (S O) timesAC (λ (m : nat) -> λ (i : nat) -> p) (lt-O-S n) (lt-O-log p n (lt-to-le-to-lt (S O) p n (prime-to-lt-SO p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb p) Hp2))) (le-S-S-to-le p n Hp1)) (le-S-S-to-le p n Hp1)) (λ (i : nat) -> λ (j : nat) -> λ (auto : lt i (S n)) -> λ (auto' : lt j (log p n)) -> refl lzero bool (andb (leb p i) (dividesb (exp p (S j)) i)))) (same-bigop (log p n) (λ (X-- : nat) -> true) (λ (X-- : nat) -> true) nat (S O) times (λ (X-- : nat) -> bigop (S n) (λ (m : nat) -> andb (leb p m) (dividesb (exp p (S X--)) m)) nat (S O) times (λ (m : nat) -> p)) (λ (X-- : nat) -> exp p (div n (exp p (S X--)))) (λ (i : nat) -> λ (auto : lt i (log p n)) -> refl lzero bool true) (λ (m : nat) -> λ (ltm : lt m (log p n)) -> λ (X-- : eq lzero bool true true) -> eq-ind-r lzero lzero nat (exp p (bigop (S n) (λ (i : nat) -> andb (leb p i) (dividesb (exp p (S m)) i)) nat O plus (λ (i : nat) -> S O))) (λ (x : nat) -> λ (X-0 : eq lzero nat x (exp p (bigop (S n) (λ (i : nat) -> andb (leb p i) (dividesb (exp p (S m)) i)) nat O plus (λ (i : nat) -> S O)))) -> eq lzero nat x (exp p (div n (exp p (S m))))) (eq-f lzero lzero nat nat (exp p) (bigop (S n) (λ (i : nat) -> andb (leb p i) (dividesb (exp p (S m)) i)) nat O plus (λ (i : nat) -> S O)) (div n (exp p (S m))) (trans-eq lzero nat (bigop (S n) (λ (i : nat) -> andb (leb p i) (dividesb (exp p (S m)) i)) nat O plus (λ (i : nat) -> S O)) (bigop (S n) (λ (i : nat) -> andb (leb (S O) i) (dividesb (exp p (S m)) i)) nat O plus (λ (i : nat) -> S O)) (div n (exp p (S m))) (same-bigop (S n) (λ (X-0 : nat) -> andb (leb p X-0) (dividesb (exp p (S m)) X-0)) (λ (X-0 : nat) -> andb (leb (S O) X-0) (dividesb (exp p (S m)) X-0)) nat O plus (λ (X-0 : nat) -> S O) (λ (X-0 : nat) -> S O) (λ (i : nat) -> λ (lti : lt i (S n)) -> match-Or lzero lzero (eq lzero bool (dividesb (exp p (S m)) i) true) (eq lzero bool (dividesb (exp p (S m)) i) false) lzero (λ (X-0 : Or lzero lzero (eq lzero bool (dividesb (exp p (S m)) i) true) (eq lzero bool (dividesb (exp p (S m)) i) false)) -> eq lzero bool (andb (leb p i) (dividesb (exp p (S m)) i)) (andb (leb (S O) i) (dividesb (exp p (S m)) i))) (λ (Hc : eq lzero bool (dividesb (exp p (S m)) i) true) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-0 : eq lzero bool x true) -> eq lzero bool (andb (leb p i) x) (andb (leb (S O) i) x)) (match-Or lzero lzero (eq lzero bool (leb p i) true) (eq lzero bool (leb p i) false) lzero (λ (X-0 : Or lzero lzero (eq lzero bool (leb p i) true) (eq lzero bool (leb p i) false)) -> eq lzero bool (andb (leb p i) true) (andb (leb (S O) i) true)) (λ (Hp3 : eq lzero bool (leb p i) true) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-0 : eq lzero bool x true) -> eq lzero bool (andb x true) (andb (leb (S O) i) true)) (eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-0 : eq lzero bool x true) -> eq lzero bool (andb true true) (andb x true)) (refl lzero bool (andb true true)) (leb (S O) i) (le-to-leb-true (S O) i (transitive-le (S O) p i (prime-to-lt-O p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X--1 : bool) -> eq lzero bool X--1 true) (refl lzero bool true) (primeb p) Hp2))) (leb-true-to-le p i (rewrite-r lzero lzero bool true (λ (X--1 : bool) -> eq lzero bool X--1 true) (refl lzero bool true) (leb p i) Hp3))))) (leb p i) Hp3) (λ (Hp3 : eq lzero bool (leb p i) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-0 : eq lzero bool x false) -> eq lzero bool (andb x true) (andb (leb (S O) i) true)) (eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-0 : eq lzero bool x false) -> eq lzero bool (andb false true) (andb x true)) (refl lzero bool (andb false true)) (leb (S O) i) (lt-to-leb-false (S O) i (not-le-to-lt (S O) i (not-to-not lzero (le (S O) i) (le p i) (λ (posi : le (S O) i) -> transitive-le p (exp p (S m)) i (eq-ind-r lzero lzero nat (exp p (S O)) (λ (x : nat) -> λ (X-0 : eq lzero nat x (exp p (S O))) -> le x (exp p (S m))) (le-exp (S O) (S m) p (prime-to-lt-O p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X--1 : bool) -> eq lzero bool X--1 true) (refl lzero bool true) (primeb p) Hp2))) (le-S-S O m (le-O-n m))) p (exp-n-1 p)) (divides-to-le (exp p (S m)) i posi (dividesb-true-to-divides (exp p (S m)) i (rewrite-r lzero lzero bool true (λ (X--1 : bool) -> eq lzero bool X--1 true) (refl lzero bool true) (dividesb (exp p (S m)) i) Hc)))) (leb-false-to-not-le p i Hp3))))) (leb p i) Hp3) (true-or-false (leb p i))) (dividesb (exp p (S m)) i) Hc) (λ (Hc : eq lzero bool (dividesb (exp p (S m)) i) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-0 : eq lzero bool x false) -> eq lzero bool (andb (leb p i) x) (andb (leb (S O) i) x)) (match-bool lzero (λ (X-0 : bool) -> eq lzero bool (andb X-0 false) (andb (leb (S O) i) false)) (match-bool lzero (λ (X-0 : bool) -> eq lzero bool (andb true false) (andb X-0 false)) (refl lzero bool (andb true false)) (refl lzero bool (andb true false)) (leb (S O) i)) (match-bool lzero (λ (X-0 : bool) -> eq lzero bool (andb false false) (andb X-0 false)) (refl lzero bool (andb false false)) (refl lzero bool (andb false false)) (leb (S O) i)) (leb p i)) (dividesb (exp p (S m)) i) Hc) (true-or-false (dividesb (exp p (S m)) i))) (λ (i : nat) -> λ (auto : lt i (S n)) -> λ (auto' : eq lzero bool (andb (leb p i) (dividesb (exp p (S m)) i)) true) -> refl lzero nat (S O))) (eq-sigma-p-div n (exp p (S m)) (lt-O-exp p (S m) (prime-to-lt-O p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X--1 : bool) -> eq lzero bool X--1 true) (refl lzero bool true) (primeb p) Hp2))))))) (bigop (S n) (λ (i : nat) -> andb (leb p i) (dividesb (exp p (S m)) i)) nat (S O) times (λ (i : nat) -> p)) (exp-sigma (S n) p (λ (X-0 : nat) -> andb (leb p X-0) (dividesb (exp p (S m)) X-0)))))))))))) (fact n) (eq-fact-pi-p n)
fact-pi-p2 : (n : nat) -> eq lzero nat (fact (times (S (S O)) n)) (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> times (exp p (times (S (S O)) (div n (exp p (S i))))) (exp p (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O)))))))
fact-pi-p2 = λ (n : nat) -> eq-ind-r lzero lzero nat (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div (times (S (S O)) n) (exp p (S i)))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div (times (S (S O)) n) (exp p (S i))))))) -> eq lzero nat x (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> times (exp p (times (S (S O)) (div n (exp p (S i))))) (exp p (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O)))))))) (same-bigop (S (times (S (S O)) n)) primeb primeb nat (S O) times (λ (X-- : nat) -> bigop (log X-- (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp X-- (div (times (S (S O)) n) (exp X-- (S i))))) (λ (X-- : nat) -> bigop (log X-- (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> times (exp X-- (times (S (S O)) (div n (exp X-- (S i))))) (exp X-- (mod (div (times (S (S O)) n) (exp X-- (S i))) (S (S O)))))) (λ (i : nat) -> λ (auto : lt i (S (times (S (S O)) n))) -> refl lzero bool (primeb i)) (λ (p : nat) -> λ (ltp : lt p (S (times (S (S O)) n))) -> λ (primep : eq lzero bool (primeb p) true) -> same-bigop (log p (times (S (S O)) n)) (λ (X-- : nat) -> true) (λ (X-- : nat) -> true) nat (S O) times (λ (X-- : nat) -> exp p (div (times (S (S O)) n) (exp p (S X--)))) (λ (X-- : nat) -> times (exp p (times (S (S O)) (div n (exp p (S X--))))) (exp p (mod (div (times (S (S O)) n) (exp p (S X--))) (S (S O))))) (λ (i : nat) -> λ (auto : lt i (log p (times (S (S O)) n))) -> refl lzero bool true) (λ (i : nat) -> λ (lti : lt i (log p (times (S (S O)) n))) -> λ (X-- : eq lzero bool true true) -> eq-ind lzero lzero nat (exp p (plus (times (S (S O)) (div n (exp p (S i)))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp p (plus (times (S (S O)) (div n (exp p (S i)))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) x-1) -> eq lzero nat (exp p (div (times (S (S O)) n) (exp p (S i)))) x-1) (eq-f lzero lzero nat nat (exp p) (div (times (S (S O)) n) (exp p (S i))) (plus (times (S (S O)) (div n (exp p (S i)))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O)))) (eq-ind-r lzero lzero nat (times (div n (exp p (S i))) (S (S O))) (λ (x : nat) -> λ (X-0 : eq lzero nat x (times (div n (exp p (S i))) (S (S O)))) -> eq lzero nat (div (times (S (S O)) n) (exp p (S i))) (plus x (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (eq-ind-r lzero lzero nat (div (times n (S (S O))) (times (exp p (S i)) (S (S O)))) (λ (x : nat) -> λ (X-0 : eq lzero nat x (div (times n (S (S O))) (times (exp p (S i)) (S (S O))))) -> eq lzero nat (div (times (S (S O)) n) (exp p (S i))) (plus (times x (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (eq-ind-r lzero lzero nat (times (S (S O)) n) (λ (x : nat) -> λ (X-0 : eq lzero nat x (times (S (S O)) n)) -> eq lzero nat (div (times (S (S O)) n) (exp p (S i))) (plus (times (div x (times (exp p (S i)) (S (S O)))) (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (eq-ind lzero lzero nat (div (div (times (S (S O)) n) (exp p (S i))) (S (S O))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (div (div (times (S (S O)) n) (exp p (S i))) (S (S O))) x-1) -> eq lzero nat (div (times (S (S O)) n) (exp p (S i))) (plus (times x-1 (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X--1 : nat) -> eq lzero nat (div X--1 (exp p (S i))) (plus (times (div (div (times (S (S O)) n) (exp p (S i))) (S (S O))) (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X--1 : nat) -> eq lzero nat (div X--1 (exp p (S i))) (plus (times (div (div (times (S (S O)) n) (exp p (S i))) (S (S O))) (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X--1 : nat) -> eq lzero nat (div (plus n X--1) (exp p (S i))) (plus (times (div (div (times (S (S O)) n) (exp p (S i))) (S (S O))) (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat O (λ (X--1 : nat) -> eq lzero nat (div (plus n (plus n X--1)) (exp p (S i))) (plus (times (div (div (times (S (S O)) n) (exp p (S i))) (S (S O))) (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat n (λ (X--1 : nat) -> eq lzero nat (div (plus n X--1) (exp p (S i))) (plus (times (div (div (times (S (S O)) n) (exp p (S i))) (S (S O))) (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus (times (div (div X--1 (exp p (S i))) (S (S O))) (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus (times (div (div X--1 (exp p (S i))) (S (S O))) (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus (times (div (div (plus n X--1) (exp p (S i))) (S (S O))) (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat O (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus (times (div (div (plus n (plus n X--1)) (exp p (S i))) (S (S O))) (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat n (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus (times (div (div (plus n X--1) (exp p (S i))) (S (S O))) (S (S O))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-r lzero lzero nat (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O)))) (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus X--1 (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O)))) (mod (div X--1 (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O)))) (mod (div X--1 (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O)))) (mod (div (plus n X--1) (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat O (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O)))) (mod (div (plus n (plus n X--1)) (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat n (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O)))) (mod (div (plus n X--1) (exp p (S i))) (S (S O))))) (rewrite-r lzero lzero nat (plus (mod (div (plus n n) (exp p (S i))) (S (S O))) (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O))))) (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) X--1) (rewrite-l lzero lzero nat (div (plus n n) (exp p (S i))) (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) X--1) (refl lzero nat (div (plus n n) (exp p (S i)))) (plus (mod (div (plus n n) (exp p (S i))) (S (S O))) (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O))))) (rewrite-l lzero lzero nat (plus (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O)))) (mod (div (plus n n) (exp p (S i))) (S (S O)))) (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) X--1) (rewrite-l lzero lzero nat (times (div (div (plus n n) (exp p (S i))) (S (S O))) (S (S O))) (λ (X--1 : nat) -> eq lzero nat (div (plus n n) (exp p (S i))) (plus X--1 (mod (div (plus n n) (exp p (S i))) (S (S O))))) (div-mod (div (plus n n) (exp p (S i))) (S (S O))) (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O)))) (commutative-times (div (div (plus n n) (exp p (S i))) (S (S O))) (S (S O)))) (plus (mod (div (plus n n) (exp p (S i))) (S (S O))) (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O))))) (commutative-plus (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O)))) (mod (div (plus n n) (exp p (S i))) (S (S O)))))) (plus (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O)))) (mod (div (plus n n) (exp p (S i))) (S (S O)))) (commutative-plus (times (S (S O)) (div (div (plus n n) (exp p (S i))) (S (S O)))) (mod (div (plus n n) (exp p (S i))) (S (S O))))) (plus n O) (plus-n-O n)) (times n O) (times-n-O n)) (times n (S O)) (times-n-Sm n O)) (times n (S (S O))) (times-n-Sm n (S O))) (times (S (S O)) n) (commutative-times (S (S O)) n)) (times (div (div (plus n n) (exp p (S i))) (S (S O))) (S (S O))) (commutative-times (div (div (plus n n) (exp p (S i))) (S (S O))) (S (S O)))) (plus n O) (plus-n-O n)) (times n O) (times-n-O n)) (times n (S O)) (times-n-Sm n O)) (times n (S (S O))) (times-n-Sm n (S O))) (times (S (S O)) n) (commutative-times (S (S O)) n)) (plus n O) (plus-n-O n)) (times n O) (times-n-O n)) (times n (S O)) (times-n-Sm n O)) (times n (S (S O))) (times-n-Sm n (S O))) (times (S (S O)) n) (commutative-times (S (S O)) n)) (div (times (S (S O)) n) (times (exp p (S i)) (S (S O)))) (eq-div-div-div-times (exp p (S i)) (S (S O)) (times (S (S O)) n) (lt-O-exp p (S i) (prime-to-lt-O p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X--1 : bool) -> eq lzero bool X--1 true) (refl lzero bool true) (primeb p) primep)))) (lt-O-S (S O)))) (times n (S (S O))) (commutative-times n (S (S O)))) (div n (exp p (S i))) (div-times-times n (exp p (S i)) (S (S O)) (lt-O-S (S O)) (lt-O-exp p (S i) (prime-to-lt-O p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X--1 : bool) -> eq lzero bool X--1 true) (refl lzero bool true) (primeb p) primep)))))) (times (S (S O)) (div n (exp p (S i)))) (commutative-times (S (S O)) (div n (exp p (S i)))))) (times (exp p (times (S (S O)) (div n (exp p (S i))))) (exp p (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (exp-plus-times p (times (S (S O)) (div n (exp p (S i)))) (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))))) (fact (times (S (S O)) n)) (fact-pi-p (times (S (S O)) n))
fact-pi-p3 : (n : nat) -> eq lzero nat (fact (times (S (S O)) n)) (times (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O)))))))
fact-pi-p3 = λ (n : nat) -> eq-ind lzero lzero nat (bigop (S (times (S (S O)) n)) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> times (bigop (log i (times (S (S O)) n)) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (times (S (S O)) (div n (exp i (S i0)))))) (bigop (log i (times (S (S O)) n)) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (mod (div (times (S (S O)) n) (exp i (S i0))) (S (S O))))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bigop (S (times (S (S O)) n)) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> times (bigop (log i (times (S (S O)) n)) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (times (S (S O)) (div n (exp i (S i0)))))) (bigop (log i (times (S (S O)) n)) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (mod (div (times (S (S O)) n) (exp i (S i0))) (S (S O))))))) x-1) -> eq lzero nat (fact (times (S (S O)) n)) x-1) (eq-ind-r lzero lzero nat (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> times (exp p (times (S (S O)) (div n (exp p (S i))))) (exp p (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> times (exp p (times (S (S O)) (div n (exp p (S i))))) (exp p (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O)))))))) -> eq lzero nat x (bigop (S (times (S (S O)) n)) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> times (bigop (log i (times (S (S O)) n)) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (times (S (S O)) (div n (exp i (S i0)))))) (bigop (log i (times (S (S O)) n)) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (mod (div (times (S (S O)) n) (exp i (S i0))) (S (S O)))))))) (same-bigop (S (times (S (S O)) n)) primeb primeb nat (S O) times (λ (X-- : nat) -> bigop (log X-- (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> times (exp X-- (times (S (S O)) (div n (exp X-- (S i))))) (exp X-- (mod (div (times (S (S O)) n) (exp X-- (S i))) (S (S O)))))) (λ (X-- : nat) -> times (bigop (log X-- (times (S (S O)) n)) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp X-- (times (S (S O)) (div n (exp X-- (S i0)))))) (bigop (log X-- (times (S (S O)) n)) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp X-- (mod (div (times (S (S O)) n) (exp X-- (S i0))) (S (S O)))))) (λ (i : nat) -> λ (auto : lt i (S (times (S (S O)) n))) -> refl lzero bool (primeb i)) (λ (p : nat) -> λ (ltp : lt p (S (times (S (S O)) n))) -> λ (primep : eq lzero bool (primeb p) true) -> times-pi (log p (times (S (S O)) n)) (λ (X-- : nat) -> true) (λ (X-- : nat) -> exp p (times (S (S O)) (div n (exp p (S X--))))) (λ (X-- : nat) -> exp p (mod (div (times (S (S O)) n) (exp p (S X--))) (S (S O)))))) (fact (times (S (S O)) n)) (fact-pi-p2 n)) (times (bigop (S (times (S (S O)) n)) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> bigop (log i (times (S (S O)) n)) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (times (S (S O)) (div n (exp i (S i0))))))) (bigop (S (times (S (S O)) n)) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> bigop (log i (times (S (S O)) n)) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (mod (div (times (S (S O)) n) (exp i (S i0))) (S (S O))))))) (times-pi (S (times (S (S O)) n)) primeb (λ (X-- : nat) -> bigop (log X-- (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp X-- (times (S (S O)) (div n (exp X-- (S i)))))) (λ (X-- : nat) -> bigop (log X-- (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp X-- (mod (div (times (S (S O)) n) (exp X-- (S i))) (S (S O))))))
pi-p-primeb4 : (n : nat) -> (X-- : lt (S O) n) -> eq lzero nat (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))))
pi-p-primeb4 = λ (n : nat) -> λ (lt1n : lt (S O) n) -> sym-eq lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (pad-bigop-nil (S (times (S (S O)) n)) (S n) primeb nat (S O) (aop lzero nat (S O) timesAC) (λ (X-- : nat) -> bigop (log X-- (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp X-- (times (S (S O)) (div n (exp X-- (S i)))))) (le-S-S n (times (S (S O)) n) (le-plus-n-r (times (S O) n) n)) (λ (i : nat) -> λ (ltn : le (S n) i) -> λ (lti : lt i (S (times (S (S O)) n))) -> or-intror lzero lzero (eq lzero bool (primeb i) false) (eq lzero nat (bigop (log i (times (S (S O)) n)) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (times (S (S O)) (div n (exp i (S i0)))))) (S O)) (eq-ind-r lzero lzero nat (S O) (λ (x : nat) -> λ (X-- : eq lzero nat x (S O)) -> eq lzero nat (bigop x (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (times (S (S O)) (div n (exp i (S i0)))))) (S O)) (eq-ind-r lzero lzero nat (times (exp i (times (S (S O)) (div n (exp i (S O))))) (bigop O (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (times (S (S O)) (div n (exp i (S i0))))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp i (times (S (S O)) (div n (exp i (S O))))) (bigop O (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (times (S (S O)) (div n (exp i (S i0)))))))) -> eq lzero nat x (S O)) (eq-ind lzero lzero nat (exp i (times (S (S O)) (div n (exp i (S O))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp i (times (S (S O)) (div n (exp i (S O))))) x-1) -> eq lzero nat x-1 (S O)) (eq-ind lzero lzero nat i (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat i x-1) -> eq lzero nat (exp i (times (S (S O)) (div n x-1))) (S O)) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (exp i (times (S (S O)) x)) (S O)) (refl lzero nat (exp i (times (S (S O)) O))) (div n i) (eq-div-O n i ltn)) (exp i (S O)) (exp-n-1 i)) (times (exp i (times (S (S O)) (div n (exp i (S O))))) (S O)) (times-n-1 (exp i (times (S (S O)) (div n (exp i (S O))))))) (bigop (S O) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (times (S (S O)) (div n (exp i (S i0)))))) (bigop-Strue O (λ (X-- : nat) -> true) nat (S O) times (λ (X-- : nat) -> exp i (times (S (S O)) (div n (exp i (S X--))))) (refl lzero bool true))) (log i (times (S (S O)) n)) (log-i-2n n i lt1n ltn (le-S-S-to-le i (times (S (S O)) n) lti)))))
pi-p-primeb5 : (n : nat) -> (X-- : lt (S O) n) -> eq lzero nat (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))))
pi-p-primeb5 = λ (n : nat) -> λ (lt1n : lt (S O) n) -> eq-ind-r lzero lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))))) -> eq lzero nat x (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))))) (same-bigop (S n) primeb primeb nat (S O) times (λ (X-- : nat) -> bigop (log X-- (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp X-- (times (S (S O)) (div n (exp X-- (S i)))))) (λ (X-- : nat) -> bigop (log X-- n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp X-- (times (S (S O)) (div n (exp X-- (S i)))))) (λ (i : nat) -> λ (auto : lt i (S n)) -> refl lzero bool (primeb i)) (λ (p : nat) -> λ (lepn : lt p (S n)) -> λ (primebp : eq lzero bool (primeb p) true) -> sym-eq lzero nat (bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))) (bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))) (pad-bigop-nil (log p (times (S (S O)) n)) (log p n) (λ (X-- : nat) -> true) nat (S O) (aop lzero nat (S O) timesAC) (λ (X-- : nat) -> exp p (times (S (S O)) (div n (exp p (S X--))))) (le-log p n (times (S (S O)) n) (prime-to-lt-SO p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb p) primebp))) (le-plus-n-r (times (S O) n) n)) (λ (i : nat) -> λ (lelog : le (log p n) i) -> λ (lti : lt i (log p (times (S (S O)) n))) -> or-intror lzero lzero (eq lzero bool true false) (eq lzero nat (exp p (times (S (S O)) (div n (exp p (S i))))) (S O)) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (exp p (times (S (S O)) x)) (S O)) (refl lzero nat (exp p (times (S (S O)) O))) (div n (exp p (S i))) (eq-div-O n (exp p (S i)) (lt-to-le-to-lt n (exp p (S (log p n))) (exp p (S i)) (lt-exp-log p n (prime-to-lt-SO p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb p) primebp)))) (le-exp (S (log p n)) (S i) p (prime-to-lt-O p (primeb-true-to-prime p (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb p) primebp))) (le-S-S (log p n) i lelog))))))))) (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (pi-p-primeb4 n lt1n)
exp-fact-2 : (n : nat) -> eq lzero nat (exp (fact n) (S (S O))) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))))
exp-fact-2 = λ (n : nat) -> eq-ind-r lzero lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div n (exp p (S i)))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (div n (exp p (S i))))))) -> eq lzero nat (exp x (S (S O))) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))))) (eq-ind lzero lzero nat (bigop (S n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp (bigop (log i n) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (div n (exp i (S i0))))) (S (S O)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bigop (S n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp (bigop (log i n) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (div n (exp i (S i0))))) (S (S O)))) x-1) -> eq lzero nat x-1 (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))))) (same-bigop (S n) primeb primeb nat (S O) times (λ (X-- : nat) -> exp (bigop (log X-- n) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp X-- (div n (exp X-- (S i0))))) (S (S O))) (λ (X-- : nat) -> bigop (log X-- n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp X-- (times (S (S O)) (div n (exp X-- (S i)))))) (λ (i : nat) -> λ (auto : lt i (S n)) -> refl lzero bool (primeb i)) (λ (p : nat) -> λ (ltp : lt p (S n)) -> λ (primebp : eq lzero bool (primeb p) true) -> sym-eq lzero nat (bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))) (exp (bigop (log p n) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp p (div n (exp p (S i0))))) (S (S O))) (trans-eq lzero nat (bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))) (bigop (log p n) (λ (x : nat) -> true) nat (S O) times (λ (x : nat) -> exp (exp p (div n (exp p (S x)))) (S (S O)))) (exp (bigop (log p n) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp p (div n (exp p (S i0))))) (S (S O))) (same-bigop (log p n) (λ (X-- : nat) -> true) (λ (X-- : nat) -> true) nat (S O) times (λ (X-- : nat) -> exp p (times (S (S O)) (div n (exp p (S X--))))) (λ (X-- : nat) -> exp (exp p (div n (exp p (S X--)))) (S (S O))) (λ (i : nat) -> λ (auto : lt i (log p n)) -> refl lzero bool true) (λ (x : nat) -> λ (ltx : lt x (log p n)) -> λ (X-- : eq lzero bool true true) -> sym-eq lzero nat (exp (exp p (div n (exp p (S x)))) (S (S O))) (exp p (times (S (S O)) (div n (exp p (S x))))) (eq-ind-r lzero lzero nat (times (div n (exp p (S x))) (S (S O))) (λ (x0 : nat) -> λ (X-0 : eq lzero nat x0 (times (div n (exp p (S x))) (S (S O)))) -> eq lzero nat (exp (exp p (div n (exp p (S x)))) (S (S O))) (exp p x0)) (exp-exp-times p (div n (exp p (S x))) (S (S O))) (times (S (S O)) (div n (exp p (S x)))) (commutative-times (S (S O)) (div n (exp p (S x))))))) (exp-pi (log p n) (S (S O)) (λ (X-- : nat) -> true) (λ (X-- : nat) -> exp p (div n (exp p (S X--)))))))) (exp (bigop (S n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> bigop (log i n) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (div n (exp i (S i0)))))) (S (S O))) (exp-pi (S n) (S (S O)) primeb (λ (X-- : nat) -> bigop (log X-- n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp X-- (div n (exp X-- (S i))))))) (fact n) (fact-pi-p n)
B : (X-n : nat) -> nat
B = λ (n : nat) -> bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (mod (div n (exp p (S i))) (S (S O)))))
Bdef : (n : nat) -> eq lzero nat (B n) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (mod (div n (exp p (S i))) (S (S O))))))
Bdef = λ (n : nat) -> refl lzero nat (B n)
B-SSSO : eq lzero nat (B (S (S (S O)))) (S (S (S (S (S (S O))))))
B-SSSO = refl lzero nat (B (S (S (S O))))
B-SSSSO : eq lzero nat (B (S (S (S (S O))))) (S (S (S (S (S (S O))))))
B-SSSSO = refl lzero nat (B (S (S (S (S O)))))
B-SSSSSO : eq lzero nat (B (S (S (S (S (S O)))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))
B-SSSSSO = refl lzero nat (B (S (S (S (S (S O))))))
B-SSSSSSO : eq lzero nat (B (S (S (S (S (S (S O))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))
B-SSSSSSO = refl lzero nat (B (S (S (S (S (S (S O)))))))
B-SSSSSSSO : eq lzero nat (B (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
B-SSSSSSSO = refl lzero nat (B (S (S (S (S (S (S (S O))))))))
B-SSSSSSSSO : eq lzero nat (B (S (S (S (S (S (S (S (S O))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
B-SSSSSSSSO = refl lzero nat (B (S (S (S (S (S (S (S (S O)))))))))
eq-fact-B : (n : nat) -> (X-- : lt (S O) n) -> eq lzero nat (fact (times (S (S O)) n)) (times (exp (fact n) (S (S O))) (B (times (S (S O)) n)))
eq-fact-B = λ (n : nat) -> λ (lt1n : lt (S O) n) -> eq-ind-r lzero lzero nat (times (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O)))))))) -> eq lzero nat x (times (exp (fact n) (S (S O))) (B (times (S (S O)) n)))) (eq-f2 lzero lzero lzero nat nat nat times (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (exp (fact n) (S (S O))) (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O)))))) (B (times (S (S O)) n)) (sym-eq lzero nat (exp (fact n) (S (S O))) (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (eq-ind-r lzero lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i)))))))) -> eq lzero nat (exp (fact n) (S (S O))) x) (exp-fact-2 n) (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (times (S (S O)) (div n (exp p (S i))))))) (pi-p-primeb5 n lt1n))) (refl lzero nat (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp p (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O)))))))) (fact (times (S (S O)) n)) (fact-pi-p3 n)
lt-SO-to-le-B-exp : (n : nat) -> (X-- : lt (S O) n) -> le (B (times (S (S O)) n)) (exp (S (S O)) (pred (times (S (S O)) n)))
lt-SO-to-le-B-exp = λ (n : nat) -> λ (lt1n : lt (S O) n) -> le-times-to-le (exp (fact n) (S (S O))) (B (times (S (S O)) n)) (exp (S (S O)) (pred (times (S (S O)) n))) (lt-O-exp (fact n) (S (S O)) (le-1-fact n)) (eq-ind lzero lzero nat (fact (times (S (S O)) n)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (fact (times (S (S O)) n)) x-1) -> le x-1 (times (exp (fact n) (S (S O))) (exp (S (S O)) (pred (times (S (S O)) n))))) (eq-ind lzero lzero nat (times (exp (S (S O)) (pred (times (S (S O)) n))) (exp (fact n) (S (S O)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (exp (S (S O)) (pred (times (S (S O)) n))) (exp (fact n) (S (S O)))) x-1) -> le (fact (times (S (S O)) n)) x-1) (eq-ind-r lzero lzero nat (times (fact n) (fact n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (fact n) (fact n))) -> le (fact (times (S (S O)) n)) (times (exp (S (S O)) (pred (times (S (S O)) n))) x)) (eq-ind lzero lzero nat (times (times (exp (S (S O)) (pred (times (S (S O)) n))) (fact n)) (fact n)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (exp (S (S O)) (pred (times (S (S O)) n))) (fact n)) (fact n)) x-1) -> le (fact (times (S (S O)) n)) x-1) (fact-to-exp n) (times (exp (S (S O)) (pred (times (S (S O)) n))) (times (fact n) (fact n))) (associative-times (exp (S (S O)) (pred (times (S (S O)) n))) (fact n) (fact n))) (exp (fact n) (S (S O))) (exp-2 (fact n))) (times (exp (fact n) (S (S O))) (exp (S (S O)) (pred (times (S (S O)) n)))) (commutative-times (exp (S (S O)) (pred (times (S (S O)) n))) (exp (fact n) (S (S O))))) (times (exp (fact n) (S (S O))) (B (times (S (S O)) n))) (eq-fact-B n lt1n))
le-B-exp : (n : nat) -> le (B (times (S (S O)) n)) (exp (S (S O)) (pred (times (S (S O)) n)))
le-B-exp = λ (n : nat) -> match-nat lzero (λ (X-- : nat) -> le (B (times (S (S O)) X--)) (exp (S (S O)) (pred (times (S (S O)) X--)))) (le-n (B (times (S (S O)) O))) (λ (n1 : nat) -> match-nat lzero (λ (X-- : nat) -> le (B (times (S (S O)) (S X--))) (exp (S (S O)) (pred (times (S (S O)) (S X--))))) (le-n (B (times (S (S O)) (S O)))) (λ (n2 : nat) -> lt-SO-to-le-B-exp (S (S n2)) (le-S-S (S O) (S n2) (lt-O-S n2))) n1) n
lt-4-to-le-B-exp : (n : nat) -> (X-- : lt (S (S (S (S O)))) n) -> le (B (times (S (S O)) n)) (exp (S (S O)) (minus (times (S (S O)) n) (S (S O))))
lt-4-to-le-B-exp = λ (n : nat) -> λ (lt4n : lt (S (S (S (S O)))) n) -> le-times-to-le (exp (fact n) (S (S O))) (B (times (S (S O)) n)) (exp (S (S O)) (minus (times (S (S O)) n) (S (S O)))) (lt-O-exp (fact n) (S (S O)) (le-1-fact n)) (eq-ind lzero lzero nat (fact (times (S (S O)) n)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (fact (times (S (S O)) n)) x-1) -> le x-1 (times (exp (fact n) (S (S O))) (exp (S (S O)) (minus (times (S (S O)) n) (S (S O)))))) (eq-ind lzero lzero nat (times (exp (S (S O)) (minus (times (S (S O)) n) (S (S O)))) (exp (fact n) (S (S O)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (exp (S (S O)) (minus (times (S (S O)) n) (S (S O)))) (exp (fact n) (S (S O)))) x-1) -> le (fact (times (S (S O)) n)) x-1) (eq-ind-r lzero lzero nat (times (fact n) (fact n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (fact n) (fact n))) -> le (fact (times (S (S O)) n)) (times (exp (S (S O)) (minus (times (S (S O)) n) (S (S O)))) x)) (eq-ind lzero lzero nat (times (times (exp (S (S O)) (minus (times (S (S O)) n) (S (S O)))) (fact n)) (fact n)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (exp (S (S O)) (minus (times (S (S O)) n) (S (S O)))) (fact n)) (fact n)) x-1) -> le (fact (times (S (S O)) n)) x-1) (lt-4-to-fact n lt4n) (times (exp (S (S O)) (minus (times (S (S O)) n) (S (S O)))) (times (fact n) (fact n))) (associative-times (exp (S (S O)) (minus (times (S (S O)) n) (S (S O)))) (fact n) (fact n))) (exp (fact n) (S (S O))) (exp-2 (fact n))) (times (exp (fact n) (S (S O))) (exp (S (S O)) (minus (times (S (S O)) n) (S (S O))))) (commutative-times (exp (S (S O)) (minus (times (S (S O)) n) (S (S O)))) (exp (fact n) (S (S O))))) (times (exp (fact n) (S (S O))) (B (times (S (S O)) n))) (eq-fact-B n (lt-to-le (S (S O)) n (lt-to-le (S (S (S O))) n (lt-to-le (S (S (S (S O)))) n lt4n)))))
lt-1-to-le-exp-B : (n : nat) -> (X-- : lt (S O) n) -> le (exp (S (S O)) (times (S (S O)) n)) (times (times (S (S O)) n) (B (times (S (S O)) n)))
lt-1-to-le-exp-B = λ (n : nat) -> λ (lt1n : lt (S O) n) -> le-times-to-le (exp (fact n) (S (S O))) (exp (S (S O)) (times (S (S O)) n)) (times (times (S (S O)) n) (B (times (S (S O)) n))) (lt-O-exp (fact n) (S (S O)) (le-1-fact n)) (eq-ind lzero lzero nat (times (times (exp (fact n) (S (S O))) (times (S (S O)) n)) (B (times (S (S O)) n))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (exp (fact n) (S (S O))) (times (S (S O)) n)) (B (times (S (S O)) n))) x-1) -> le (times (exp (fact n) (S (S O))) (exp (S (S O)) (times (S (S O)) n))) x-1) (eq-ind-r lzero lzero nat (times (times (S (S O)) n) (exp (fact n) (S (S O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (times (S (S O)) n) (exp (fact n) (S (S O))))) -> le (times (exp (fact n) (S (S O))) (exp (S (S O)) (times (S (S O)) n))) (times x (B (times (S (S O)) n)))) (eq-ind-r lzero lzero nat (times (times (S (S O)) n) (times (exp (fact n) (S (S O))) (B (times (S (S O)) n)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (times (S (S O)) n) (times (exp (fact n) (S (S O))) (B (times (S (S O)) n))))) -> le (times (exp (fact n) (S (S O))) (exp (S (S O)) (times (S (S O)) n))) x) (eq-ind lzero lzero nat (fact (times (S (S O)) n)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (fact (times (S (S O)) n)) x-1) -> le (times (exp (fact n) (S (S O))) (exp (S (S O)) (times (S (S O)) n))) (times (times (S (S O)) n) x-1)) (eq-ind lzero lzero nat (times (exp (S (S O)) (times (S (S O)) n)) (exp (fact n) (S (S O)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (exp (S (S O)) (times (S (S O)) n)) (exp (fact n) (S (S O)))) x-1) -> le x-1 (times (times (S (S O)) n) (fact (times (S (S O)) n)))) (exp-to-fact2 n (lt-to-le (S O) n lt1n)) (times (exp (fact n) (S (S O))) (exp (S (S O)) (times (S (S O)) n))) (commutative-times (exp (S (S O)) (times (S (S O)) n)) (exp (fact n) (S (S O))))) (times (exp (fact n) (S (S O))) (B (times (S (S O)) n))) (eq-fact-B n lt1n)) (times (times (times (S (S O)) n) (exp (fact n) (S (S O)))) (B (times (S (S O)) n))) (associative-times (times (S (S O)) n) (exp (fact n) (S (S O))) (B (times (S (S O)) n)))) (times (exp (fact n) (S (S O))) (times (S (S O)) n)) (commutative-times (exp (fact n) (S (S O))) (times (S (S O)) n))) (times (exp (fact n) (S (S O))) (times (times (S (S O)) n) (B (times (S (S O)) n)))) (associative-times (exp (fact n) (S (S O))) (times (S (S O)) n) (B (times (S (S O)) n))))
le-exp-B : (n : nat) -> (X-- : lt O n) -> le (exp (S (S O)) (times (S (S O)) n)) (times (times (S (S O)) n) (B (times (S (S O)) n)))
le-exp-B = λ (n : nat) -> λ (posn : lt O n) -> match-le (S O) lzero (λ (X-- : nat) -> λ (X-0 : le (S O) X--) -> le (exp (S (S O)) (times (S (S O)) X--)) (times (times (S (S O)) X--) (B (times (S (S O)) X--)))) (le-n (exp (S (S O)) (times (S (S O)) (S O)))) (λ (m : nat) -> λ (lt1m : le (S O) m) -> lt-1-to-le-exp-B (S m) (le-S-S (S O) m lt1m)) n posn