-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmatita-arithmetics-chebyshev-chebyshev-theta.agda
58 lines (43 loc) · 61.7 KB
/
matita-arithmetics-chebyshev-chebyshev-theta.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
open import Agda.Primitive
open import matita-arithmetics-factorial
open import matita-arithmetics-gcd
open import matita-arithmetics-sigma-pi
open import matita-arithmetics-binomial
open import matita-arithmetics-div-and-mod
open import matita-arithmetics-bigops
open import matita-arithmetics-primes
open import matita-basics-bool
open import matita-basics-logic
open import matita-arithmetics-chebyshev-chebyshev-psi
open import matita-arithmetics-exp
open import matita-arithmetics-nat
theta : (X-- : nat) -> nat
theta = λ (n : nat) -> bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)
theta-def : (n : nat) -> eq lzero nat (theta n) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))
theta-def = λ (n : nat) -> refl lzero nat (theta n)
lt-O-theta : (n : nat) -> lt O (theta n)
lt-O-theta = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> lt O (theta X-x-365)) (le-n (S O)) (λ (n1 : nat) -> λ (Hind : lt O (theta n1)) -> match-Or lzero lzero (eq lzero bool (primeb (S n1)) true) (eq lzero bool (primeb (S n1)) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (primeb (S n1)) true) (eq lzero bool (primeb (S n1)) false)) -> lt O (theta (S n1))) (λ (Hc : eq lzero bool (primeb (S n1)) true) -> eq-ind-r lzero lzero nat (bigop (S (S n1)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (S n1)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) -> lt O x) (eq-ind-r lzero lzero nat (times (S n1) (bigop (S n1) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S n1) (bigop (S n1) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)))) -> lt O x) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> lt x (times (S n1) (bigop (S n1) (λ (i : nat) -> primeb i) nat (S x) times (λ (i : nat) -> i)))) (lt-times O (S n1) O (bigop (S n1) (λ (i : nat) -> primeb i) nat (S (times O O)) times (λ (i : nat) -> i)) (lt-O-S n1) Hind) O (times-n-O O)) (bigop (S (S n1)) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop-Strue (S n1) primeb nat (S O) times (λ (X-- : nat) -> X--) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb (S n1)) Hc))) (theta (S n1)) (theta-def (S n1))) (λ (Hc : eq lzero bool (primeb (S n1)) false) -> eq-ind-r lzero lzero nat (bigop (S (S n1)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (S n1)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) -> lt O x) (eq-ind-r lzero lzero nat (bigop (S n1) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n1) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i))) -> lt O x) Hind (bigop (S (S n1)) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop-Sfalse (S n1) primeb nat (S O) times (λ (X-- : nat) -> X--) (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (primeb (S n1)) Hc))) (theta (S n1)) (theta-def (S n1))) (true-or-false (primeb (S n1)))) n
divides-fact-to-divides : (p : nat) -> (n : nat) -> (X-- : prime p) -> (X--1 : divides p (fact n)) -> ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m n)) (divides p m))
divides-fact-to-divides = λ (p : nat) -> λ (n : nat) -> λ (primep : prime p) -> nat-ind lzero (λ (X-x-365 : nat) -> (X-- : divides p (fact X-x-365)) -> ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m X-x-365)) (divides p m))) (λ (H : divides p (S O)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m O)) (divides p m))) (absurd lzero (le p (S O)) (divides-to-le p (S O) (lt-O-S O) H) (lt-to-not-le (S O) p (prime-to-lt-SO p primep)))) (λ (n1 : nat) -> λ (Hind : (X-- : divides p (fact n1)) -> ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m n1)) (divides p m))) -> eq-ind-r lzero lzero nat (times (S n1) (fact n1)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S n1) (fact n1))) -> (X--1 : divides p x) -> ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m (S n1))) (divides p m))) (λ (Hdiv : divides p (times (S n1) (fact n1))) -> match-Or lzero lzero (divides p (S n1)) (divides p (fact n1)) lzero (λ (X-- : Or lzero lzero (divides p (S n1)) (divides p (fact n1))) -> ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m (S n1))) (divides p m))) (λ (Hcase : divides p (S n1)) -> ex-intro lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m (S n1))) (divides p m)) (S n1) (conj lzero lzero (And lzero lzero (lt O (S n1)) (le (S n1) (S n1))) (divides p (S n1)) (conj lzero lzero (lt O (S n1)) (le (S n1) (S n1)) (lt-O-S n1) (le-n (S n1))) Hcase)) (λ (Hcase : divides p (fact n1)) -> match-ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m n1)) (divides p m)) lzero (λ (X-- : ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m n1)) (divides p m))) -> ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m (S n1))) (divides p m))) (λ (a : nat) -> λ (X-clearme : And lzero lzero (And lzero lzero (lt O a) (le a n1)) (divides p a)) -> match-And lzero lzero (And lzero lzero (lt O a) (le a n1)) (divides p a) lzero (λ (X-- : And lzero lzero (And lzero lzero (lt O a) (le a n1)) (divides p a)) -> ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m (S n1))) (divides p m))) (λ (X-clearme0 : And lzero lzero (lt O a) (le a n1)) -> match-And lzero lzero (lt O a) (le a n1) lzero (λ (X-- : And lzero lzero (lt O a) (le a n1)) -> (X--1 : divides p a) -> ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m (S n1))) (divides p m))) (λ (posa : lt O a) -> λ (lea : le a n1) -> λ (diva : divides p a) -> ex-intro lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m (S n1))) (divides p m)) a (conj lzero lzero (And lzero lzero (lt O a) (le a (S n1))) (divides p a) (conj lzero lzero (lt O a) (le a (S n1)) posa (le-S a n1 lea)) diva)) X-clearme0) X-clearme) (Hind Hcase)) (divides-times-to-divides p (S n1) (fact n1) primep Hdiv)) (fact (S n1)) (factS n1)) n
divides-fact-to-le : (p : nat) -> (n : nat) -> (X-- : prime p) -> (X--1 : divides p (fact n)) -> le p n
divides-fact-to-le = λ (p : nat) -> λ (n : nat) -> λ (primep : prime p) -> λ (divp : divides p (fact n)) -> match-ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m n)) (divides p m)) lzero (λ (X-- : ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt O m) (le m n)) (divides p m))) -> le p n) (λ (a : nat) -> λ (X-clearme : And lzero lzero (And lzero lzero (lt O a) (le a n)) (divides p a)) -> match-And lzero lzero (And lzero lzero (lt O a) (le a n)) (divides p a) lzero (λ (X-- : And lzero lzero (And lzero lzero (lt O a) (le a n)) (divides p a)) -> le p n) (λ (X-clearme0 : And lzero lzero (lt O a) (le a n)) -> match-And lzero lzero (lt O a) (le a n) lzero (λ (X-- : And lzero lzero (lt O a) (le a n)) -> (X--1 : divides p a) -> le p n) (λ (posa : lt O a) -> λ (lea : le a n) -> λ (diva : divides p a) -> transitive-le p a n (divides-to-le p a posa diva) lea) X-clearme0) X-clearme) (divides-fact-to-divides p n primep divp)
prime-to-divides-M : (m : nat) -> (p : nat) -> (X-- : prime p) -> (X--1 : lt (S m) p) -> (X--2 : le p (S (times (S (S O)) m))) -> divides p (M m)
prime-to-divides-M = λ (m : nat) -> λ (p : nat) -> λ (primep : prime p) -> λ (lemp : lt (S m) p) -> λ (lep : le p (S (times (S (S O)) m))) -> eq-ind-r lzero lzero nat (bc (S (times (S (S O)) m)) m) (λ (x : nat) -> λ (X-- : eq lzero nat x (bc (S (times (S (S O)) m)) m)) -> divides p x) (eq-ind-r lzero lzero nat (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (minus (S (times (S (S O)) m)) m))))) -> divides p x) (match-divides (times (fact m) (fact (minus (S (times (S (S O)) m)) m))) (fact (S (times (S (S O)) m))) lzero (λ (X-- : divides (times (fact m) (fact (minus (S (times (S (S O)) m)) m))) (fact (S (times (S (S O)) m)))) -> divides p (div (fact (S (times (S (S O)) m))) (times (fact m) (fact (minus (S (times (S (S O)) m)) m))))) (λ (q : nat) -> λ (Hq : eq lzero nat (fact (S (times (S (S O)) m))) (times (times (fact m) (fact (minus (S (times (S (S O)) m)) m))) q)) -> eq-ind-r lzero lzero nat (times (times (fact m) (fact (minus (S (times (S (S O)) m)) m))) q) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (times (fact m) (fact (minus (S (times (S (S O)) m)) m))) q)) -> divides p (div x (times (fact m) (fact (minus (S (times (S (S O)) m)) m))))) (eq-ind-r lzero lzero nat (times q (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times q (times (fact m) (fact (minus (S (times (S (S O)) m)) m))))) -> divides p (div x (times (fact m) (fact (minus (S (times (S (S O)) m)) m))))) (eq-ind-r lzero lzero nat q (λ (x : nat) -> λ (X-- : eq lzero nat x q) -> divides p x) (match-Or lzero lzero (divides p (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (divides p q) lzero (λ (X-- : Or lzero lzero (divides p (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (divides p q)) -> divides p q) (λ (Hdiv : divides p (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> divides p q) (match-Or lzero lzero (divides p (fact m)) (divides p (fact (minus (S (times (S (S O)) m)) m))) lzero (λ (X-- : Or lzero lzero (divides p (fact m)) (divides p (fact (minus (S (times (S (S O)) m)) m)))) -> False lzero) (λ (Hdiv0 : divides p (fact m)) -> absurd lzero (le p m) (divides-fact-to-le p m primep Hdiv0) (lt-to-not-le m p (lt-to-le (S m) p lemp))) (λ (Hdiv0 : divides p (fact (minus (S (times (S (S O)) m)) m))) -> absurd lzero (le p (S m)) (divides-fact-to-le p (S m) primep (eq-ind-r lzero lzero nat (minus (S (times (S (S O)) m)) m) (λ (x : nat) -> λ (X-- : eq lzero nat x (minus (S (times (S (S O)) m)) m)) -> divides p (fact x)) Hdiv0 (S m) (eq-ind lzero lzero nat m (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat m x-1) -> eq lzero nat (S m) (minus (S (plus m x-1)) m)) (eq-ind-r lzero lzero nat (plus m (S m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus m (S m))) -> eq lzero nat (S m) (minus x m)) (eq-ind-r lzero lzero nat (plus (S m) m) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S m) m)) -> eq lzero nat (S m) (minus x m)) (minus-plus-m-m (S m) m) (plus m (S m)) (commutative-plus m (S m))) (S (plus m m)) (plus-n-Sm m m)) (plus m O) (plus-n-O m)))) (lt-to-not-le (S m) p lemp)) (divides-times-to-divides p (fact m) (fact (minus (S (times (S (S O)) m)) m)) primep Hdiv))) (λ (auto : divides p q) -> auto) (divides-times-to-divides p (times (fact m) (fact (minus (S (times (S (S O)) m)) m))) q primep (eq-ind lzero lzero nat (fact (S (times (S (S O)) m))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (fact (S (times (S (S O)) m))) x-1) -> divides p x-1) (divides-fact (S (times (S (S O)) m)) p (prime-to-lt-O p primep) lep) (times (times (fact m) (fact (minus (S (times (S (S O)) m)) m))) q) Hq))) (div (times q (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (div-times q (times (fact m) (fact (minus (S (times (S (S O)) m)) m))) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> lt x (times (fact m) (fact (minus (S (times (S (S O)) m)) m)))) (lt-times O (fact m) O (fact (minus (S (times (S (S O)) m)) m)) (le-1-fact m) (le-1-fact (minus (S (times (S (S O)) m)) m))) O (times-n-O O)))) (times (times (fact m) (fact (minus (S (times (S (S O)) m)) m))) q) (commutative-times (times (fact m) (fact (minus (S (times (S (S O)) m)) m))) q)) (fact (S (times (S (S O)) m))) Hq) (bc2 (S (times (S (S O)) m)) m (eq-ind lzero lzero nat m (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat m x-1) -> le m (S (plus m x-1))) (eq-coerc lzero (le (minus (S (plus m m)) (plus O (S m))) (S (plus m m))) (le m (S (plus m m))) (minus-le (S (plus m m)) (plus O (S m))) (rewrite-r lzero (lsuc lzero) nat (plus m (S m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus X-- (plus O (S m))) X--) (le m X--)) (rewrite-r lzero (lsuc lzero) nat (minus m O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus m (S m))) (le m (plus m (S m)))) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus m (S m))) (le m (plus m (S m)))) (refl (lsuc lzero) (Set (lzero)) (le m (plus m (S m)))) (minus m O) (minus-n-O m)) (minus (plus m (S m)) (plus O (S m))) (minus-plus-plus-l m O (S m))) (S (plus m m)) (plus-n-Sm m m))) (plus m O) (plus-n-O m)))) (bc (S (times (S (S O)) m)) m) (bceq (S (times (S (S O)) m)) m)) (M m) (Mdef m)
divides-pi-p-M1 : (m : nat) -> (i : nat) -> (X-- : le i (S (S (times (S (S O)) m)))) -> divides (bigop i (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (M m)
divides-pi-p-M1 = λ (m : nat) -> λ (i : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (X-- : le X-x-365 (S (S (times (S (S O)) m)))) -> divides (bigop X-x-365 (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (M m)) (λ (X-- : le O (S (S (times (S (S O)) m)))) -> quotient (bigop O (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (M m) (M m) (eq-ind-r lzero lzero nat (times (M m) (bigop O (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p))) (λ (x : nat) -> λ (X-0 : eq lzero nat x (times (M m) (bigop O (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)))) -> eq lzero nat (M m) x) (times-n-1 (M m)) (times (bigop O (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (M m)) (commutative-times (bigop O (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (M m)))) (λ (n : nat) -> λ (Hind : (X-- : le n (S (S (times (S (S O)) m)))) -> divides (bigop n (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (M m)) -> λ (len : le (S n) (S (S (times (S (S O)) m)))) -> match-Or lzero lzero (eq lzero bool (andb (leb (S (S m)) n) (primeb n)) true) (eq lzero bool (andb (leb (S (S m)) n) (primeb n)) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (andb (leb (S (S m)) n) (primeb n)) true) (eq lzero bool (andb (leb (S (S m)) n) (primeb n)) false)) -> divides (bigop (S n) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (M m)) (λ (Hc : eq lzero bool (andb (leb (S (S m)) n) (primeb n)) true) -> eq-ind-r lzero lzero nat (times n (bigop n (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times n (bigop n (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)))) -> divides x (M m)) (divides-to-divides-times n (bigop n (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)) (M m) (primeb-true-to-prime n (andb-true-r (leb (S (S m)) n) (primeb n) Hc)) (nat-ind lzero (λ (X-x-365 : nat) -> (X-- : le X-x-365 n) -> Not lzero (divides n (bigop X-x-365 (λ (p0 : nat) -> andb (leb (S (S m)) p0) (primeb p0)) nat (S O) times (λ (p0 : nat) -> p0)))) (λ (X-- : le O n) -> not-to-not lzero (divides n (S O)) (le n (S O)) (divides-to-le n (S O) (lt-O-S O)) (lt-to-not-le (S O) n (prime-to-lt-SO n (primeb-true-to-prime n (andb-true-r (leb (S (S m)) n) (primeb n) Hc))))) (λ (n1 : nat) -> λ (Hind1 : (X-- : le n1 n) -> Not lzero (divides n (bigop n1 (λ (p0 : nat) -> andb (leb (S (S m)) p0) (primeb p0)) nat (S O) times (λ (p0 : nat) -> p0)))) -> λ (Hn1 : le (S n1) n) -> match-Or lzero lzero (eq lzero bool (andb (leb (S (S m)) n1) (primeb n1)) true) (eq lzero bool (andb (leb (S (S m)) n1) (primeb n1)) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (andb (leb (S (S m)) n1) (primeb n1)) true) (eq lzero bool (andb (leb (S (S m)) n1) (primeb n1)) false)) -> Not lzero (divides n (bigop (S n1) (λ (p0 : nat) -> andb (leb (S (S m)) p0) (primeb p0)) nat (S O) times (λ (p0 : nat) -> p0)))) (λ (Hc1 : eq lzero bool (andb (leb (S (S m)) n1) (primeb n1)) true) -> eq-ind-r lzero lzero nat (times n1 (bigop n1 (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times n1 (bigop n1 (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)))) -> Not lzero (divides n x)) (nmk lzero (divides n (times n1 (bigop n1 (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)))) (λ (Habs : divides n (times n1 (bigop n1 (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)))) -> match-Or lzero lzero (divides n n1) (divides n (bigop n1 (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0))) lzero (λ (X-- : Or lzero lzero (divides n n1) (divides n (bigop n1 (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)))) -> False lzero) (λ (Habs0 : divides n n1) -> absurd lzero (le (S n1) n) Hn1 (le-to-not-lt n n1 (divides-to-le n n1 (prime-to-lt-O n1 (primeb-true-to-prime n1 (andb-true-r (leb (S (S m)) n1) (primeb n1) Hc1))) Habs0))) (λ (Habs0 : divides n (bigop n1 (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0))) -> absurd lzero (divides n (bigop n1 (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0))) Habs0 (Hind1 (lt-to-le n1 n Hn1))) (divides-times-to-divides n n1 (bigop n1 (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)) (primeb-true-to-prime n (andb-true-r (leb (S (S m)) n) (primeb n) Hc)) Habs))) (bigop (S n1) (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)) (bigop-Strue n1 (λ (X-- : nat) -> andb (leb (S (S m)) X--) (primeb X--)) nat (S O) times (λ (X-- : nat) -> X--) Hc1)) (λ (Hc1 : eq lzero bool (andb (leb (S (S m)) n1) (primeb n1)) false) -> eq-ind-r lzero lzero nat (bigop n1 (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop n1 (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0))) -> Not lzero (divides n x)) (Hind1 (lt-to-le n1 n Hn1)) (bigop (S n1) (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)) (bigop-Sfalse n1 (λ (X-- : nat) -> andb (leb (S (S m)) X--) (primeb X--)) nat (S O) times (λ (X-- : nat) -> X--) (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (andb (leb (S (S m)) n1) (primeb n1)) Hc1))) (true-or-false (andb (leb (S (S m)) n1) (primeb n1)))) n (le-n n)) (prime-to-divides-M m n (primeb-true-to-prime n (andb-true-r (leb (S (S m)) n) (primeb n) Hc)) (leb-true-to-le (S (S m)) n (andb-true-l (leb (S (S m)) n) (primeb n) Hc)) (le-S-S-to-le n (S (times (S (S O)) m)) len)) (Hind (lt-to-le n (S (S (times (S (S O)) m))) len))) (bigop (S n) (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)) (bigop-Strue n (λ (X-- : nat) -> andb (leb (S (S m)) X--) (primeb X--)) nat (S O) times (λ (X-- : nat) -> X--) Hc)) (λ (Hc : eq lzero bool (andb (leb (S (S m)) n) (primeb n)) false) -> eq-ind-r lzero lzero nat (bigop n (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop n (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0))) -> divides x (M m)) (Hind (lt-to-le n (S (S (times (S (S O)) m))) len)) (bigop (S n) (λ (i0 : nat) -> andb (leb (S (S m)) i0) (primeb i0)) nat (S O) times (λ (i0 : nat) -> i0)) (bigop-Sfalse n (λ (X-- : nat) -> andb (leb (S (S m)) X--) (primeb X--)) nat (S O) times (λ (X-- : nat) -> X--) (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (andb (leb (S (S m)) n) (primeb n)) Hc))) (true-or-false (andb (leb (S (S m)) n) (primeb n)))) i
divides-pi-p-M : (m : nat) -> divides (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (M m)
divides-pi-p-M = λ (m : nat) -> divides-pi-p-M1 m (S (S (times (S (S O)) m))) (le-n (S (S (times (S (S O)) m))))
theta-pi-p-theta : (m : nat) -> eq lzero nat (theta (S (times (S (S O)) m))) (times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (theta (S m)))
theta-pi-p-theta = λ (m : nat) -> eq-ind-r lzero lzero nat (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) -> eq lzero nat x (times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (theta (S m)))) (eq-ind-r lzero lzero nat (bigop (S (S m)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (S m)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) -> eq lzero nat (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) (times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) x)) (eq-ind lzero lzero nat (bigop (minus (S (S (times (S (S O)) m))) O) (λ (i : nat) -> primeb (plus i O)) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> plus i O)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bigop (minus (S (S (times (S (S O)) m))) O) (λ (i : nat) -> primeb (plus i O)) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> plus i O)) x-1) -> eq lzero nat x-1 (times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (bigop (S (S m)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)))) (eq-ind-r lzero lzero nat (op lzero nat (S O) timesA (bigop (minus (S (S (times (S (S O)) m))) (S (S m))) (λ (i : nat) -> primeb (plus i (S (S m)))) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> plus i (S (S m)))) (bigop (minus (S (S m)) O) (λ (i : nat) -> primeb (plus i O)) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> plus i O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (op lzero nat (S O) timesA (bigop (minus (S (S (times (S (S O)) m))) (S (S m))) (λ (i : nat) -> primeb (plus i (S (S m)))) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> plus i (S (S m)))) (bigop (minus (S (S m)) O) (λ (i : nat) -> primeb (plus i O)) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> plus i O)))) -> eq lzero nat x (times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (bigop (S (S m)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)))) (eq-f2 lzero lzero lzero nat nat nat (op lzero nat (S O) timesA) (bigop (minus (S (S (times (S (S O)) m))) (S (S m))) (λ (i : nat) -> primeb (plus i (S (S m)))) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> plus i (S (S m)))) (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (bigop (minus (S (S m)) O) (λ (i : nat) -> primeb (plus i O)) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> plus i O)) (bigop (S (S m)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) (eq-ind-r lzero lzero nat (bigop (S (S (times (S (S O)) m))) (λ (i : nat) -> andb (leb (S (S m)) i) (primeb i)) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> i)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (S (times (S (S O)) m))) (λ (i : nat) -> andb (leb (S (S m)) i) (primeb i)) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> i))) -> eq lzero nat x (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p))) (refl lzero nat (bigop (S (S (times (S (S O)) m))) (λ (i : nat) -> andb (leb (S (S m)) i) (primeb i)) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> i))) (bigop (minus (S (S (times (S (S O)) m))) (S (S m))) (λ (i : nat) -> primeb (plus i (S (S m)))) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> plus i (S (S m)))) (bigop-I-gen (S (S m)) (S (S (times (S (S O)) m))) primeb nat (S O) timesA (λ (X-- : nat) -> X--) (eq-coerc lzero (le (minus (plus (S (S (times m (S O)))) (times m (S O))) (plus (times m O) (times m (S O)))) (plus (S (S (times m (S O)))) (times m (S O)))) (le (S (S m)) (S (S (times (S (S O)) m)))) (minus-le (plus (S (S (times m (S O)))) (times m (S O))) (plus (times m O) (times m (S O)))) (rewrite-r lzero (lsuc lzero) nat (times m (S (S O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (S (S (times m (S O)))) (times m (S O))) (plus (times m O) (times m (S O)))) (plus (S (S (times m (S O)))) (times m (S O)))) (le (S (S m)) (S (S X--)))) (rewrite-l lzero (lsuc lzero) nat (plus m (times m (S O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (S (S (times m (S O)))) (times m (S O))) (plus (times m O) (times m (S O)))) (plus (S (S (times m (S O)))) (times m (S O)))) (le (S (S m)) (S (S X--)))) (rewrite-l lzero (lsuc lzero) nat (plus m (times m O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (S (S X--)) X--) (plus (times m O) X--)) (plus (S (S X--)) X--)) (le (S (S m)) (S (S (plus m X--))))) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (S (S (plus m X--))) (plus m X--)) (plus X-- (plus m X--))) (plus (S (S (plus m X--))) (plus m X--))) (le (S (S m)) (S (S (plus m (plus m X--)))))) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (S (S X--)) X--) (plus O X--)) (plus (S (S X--)) X--)) (le (S (S m)) (S (S (plus m X--))))) (rewrite-r lzero (lsuc lzero) nat (plus m (S m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (S (S m)) m) (plus O m)) (plus (S (S m)) m)) (le (S (S m)) (S X--))) (rewrite-r lzero (lsuc lzero) nat (plus m (S (S m))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (S (S m)) m) (plus O m)) (plus (S (S m)) m)) (le (S (S m)) X--)) (rewrite-r lzero (lsuc lzero) nat (minus (S (S m)) O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus (S (S m)) m)) (le (S (S m)) (plus m (S (S m))))) (rewrite-l lzero (lsuc lzero) nat (S (S m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus (S (S m)) m)) (le (S (S m)) (plus m (S (S m))))) (rewrite-r lzero (lsuc lzero) nat (plus m (S (S m))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (S m)) X--) (le (S (S m)) (plus m (S (S m))))) (refl (lsuc lzero) (Set (lzero)) (le (S (S m)) (plus m (S (S m))))) (plus (S (S m)) m) (commutative-plus (S (S m)) m)) (minus (S (S m)) O) (minus-n-O (S (S m)))) (minus (plus (S (S m)) m) (plus O m)) (minus-plus-plus-l (S (S m)) O m)) (S (plus m (S m))) (plus-n-Sm m (S m))) (S (plus m m)) (plus-n-Sm m m)) (plus m O) (plus-n-O m)) (times m O) (times-n-O m)) (times m (S O)) (times-n-Sm m O)) (times m (S (S O))) (times-n-Sm m (S O))) (times (S (S O)) m) (commutative-times (S (S O)) m))))) (bigop-I (S (S m)) primeb nat (S O) timesA (λ (X-- : nat) -> X--))) (bigop (minus (S (S (times (S (S O)) m))) O) (λ (i : nat) -> primeb (plus i O)) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> plus i O)) (bigop-sumI O (S (S m)) (S (S (times (S (S O)) m))) (λ (p : nat) -> primeb p) nat (S O) timesA (λ (p : nat) -> p) (le-O-n (S (S m))) (le-S-S (S m) (S (times (S (S O)) m)) (le-S-S m (times (S (S O)) m) (eq-coerc lzero (le (minus (plus (times m (S O)) (times m (S O))) (plus (times m O) (times m (S O)))) (plus (times m (S O)) (times m (S O)))) (le m (times (S (S O)) m)) (minus-le (plus (times m (S O)) (times m (S O))) (plus (times m O) (times m (S O)))) (rewrite-r lzero (lsuc lzero) nat (times m (S (S O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (times m (S O)) (times m (S O))) (plus (times m O) (times m (S O)))) (plus (times m (S O)) (times m (S O)))) (le m X--)) (rewrite-l lzero (lsuc lzero) nat (plus m (times m (S O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (times m (S O)) (times m (S O))) (plus (times m O) (times m (S O)))) (plus (times m (S O)) (times m (S O)))) (le m X--)) (rewrite-l lzero (lsuc lzero) nat (plus m (times m O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus X-- X--) (plus (times m O) X--)) (plus X-- X--)) (le m (plus m X--))) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (plus m X--) (plus m X--)) (plus X-- (plus m X--))) (plus (plus m X--) (plus m X--))) (le m (plus m (plus m X--)))) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus X-- X--) (plus O X--)) (plus X-- X--)) (le m (plus m X--))) (rewrite-r lzero (lsuc lzero) nat (minus m O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus m m)) (le m (plus m m))) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus m m)) (le m (plus m m))) (refl (lsuc lzero) (Set (lzero)) (le m (plus m m))) (minus m O) (minus-n-O m)) (minus (plus m m) (plus O m)) (minus-plus-plus-l m O m)) (plus m O) (plus-n-O m)) (times m O) (times-n-O m)) (times m (S O)) (times-n-Sm m O)) (times m (S (S O))) (times-n-Sm m (S O))) (times (S (S O)) m) (commutative-times (S (S O)) m))))))) (bigop (S (S (times (S (S O)) m))) (λ (i : nat) -> primeb i) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> i)) (bigop-I (S (S (times (S (S O)) m))) primeb nat (S O) timesA (λ (X-- : nat) -> X--))) (theta (S m)) (theta-def (S m))) (theta (S (times (S (S O)) m))) (theta-def (S (times (S (S O)) m)))
div-theta-theta : (m : nat) -> eq lzero nat (div (theta (S (times (S (S O)) m))) (theta (S m))) (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p))
div-theta-theta = λ (m : nat) -> div-mod-spec-to-eq (theta (S (times (S (S O)) m))) (theta (S m)) (div (theta (S (times (S (S O)) m))) (theta (S m))) (mod (theta (S (times (S (S O)) m))) (theta (S m))) (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) O (div-mod-spec-div-mod (theta (S (times (S (S O)) m))) (theta (S m)) (lt-O-theta (S m))) (div-mod-spec-intro (theta (S (times (S (S O)) m))) (theta (S m)) (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) O (lt-O-theta (S m)) (eq-ind lzero lzero nat (times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (theta (S m))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (theta (S m))) x-1) -> eq lzero nat (theta (S (times (S (S O)) m))) x-1) (theta-pi-p-theta m) (plus (times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (theta (S m))) O) (plus-n-O (times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (theta (S m))))))
le-theta-M-theta : (m : nat) -> le (theta (S (times (S (S O)) m))) (times (M m) (theta (S m)))
le-theta-M-theta = λ (m : nat) -> eq-ind-r lzero lzero nat (times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (theta (S m))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (theta (S m)))) -> le x (times (M m) (theta (S m)))) (le-times (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (M m) (theta (S m)) (theta (S m)) (divides-to-le (bigop (S (S (times (S (S O)) m))) (λ (p : nat) -> andb (leb (S (S m)) p) (primeb p)) nat (S O) times (λ (p : nat) -> p)) (M m) (lt-O-bc (S (times (S (S O)) m)) m (lt-to-le m (S (times (S (S O)) m)) (le-S-S m (times (S (S O)) m) (eq-coerc lzero (le (minus (plus (times m (S O)) (times m (S O))) (plus (times m O) (times m (S O)))) (plus (times m (S O)) (times m (S O)))) (le m (times (S (S O)) m)) (minus-le (plus (times m (S O)) (times m (S O))) (plus (times m O) (times m (S O)))) (rewrite-r lzero (lsuc lzero) nat (times m (S (S O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (times m (S O)) (times m (S O))) (plus (times m O) (times m (S O)))) (plus (times m (S O)) (times m (S O)))) (le m X--)) (rewrite-l lzero (lsuc lzero) nat (plus m (times m (S O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (times m (S O)) (times m (S O))) (plus (times m O) (times m (S O)))) (plus (times m (S O)) (times m (S O)))) (le m X--)) (rewrite-l lzero (lsuc lzero) nat (plus m (times m O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus X-- X--) (plus (times m O) X--)) (plus X-- X--)) (le m (plus m X--))) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus (plus m X--) (plus m X--)) (plus X-- (plus m X--))) (plus (plus m X--) (plus m X--))) (le m (plus m (plus m X--)))) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (plus X-- X--) (plus O X--)) (plus X-- X--)) (le m (plus m X--))) (rewrite-r lzero (lsuc lzero) nat (minus m O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus m m)) (le m (plus m m))) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus m m)) (le m (plus m m))) (refl (lsuc lzero) (Set (lzero)) (le m (plus m m))) (minus m O) (minus-n-O m)) (minus (plus m m) (plus O m)) (minus-plus-plus-l m O m)) (plus m O) (plus-n-O m)) (times m O) (times-n-O m)) (times m (S O)) (times-n-Sm m O)) (times m (S (S O))) (times-n-Sm m (S O))) (times (S (S O)) m) (commutative-times (S (S O)) m)))))) (divides-pi-p-M m)) (le-n (theta (S m)))) (theta (S (times (S (S O)) m))) (theta-pi-p-theta m)
lt-O-to-le-theta-exp-theta : (m : nat) -> (X-- : lt O m) -> lt (theta (S (times (S (S O)) m))) (times (exp (S (S O)) (times (S (S O)) m)) (theta (S m)))
lt-O-to-le-theta-exp-theta = λ (m : nat) -> λ (posm : lt O m) -> le-to-lt-to-lt (theta (S (times (S (S O)) m))) (times (M m) (theta (S m))) (times (exp (S (S O)) (times (S (S O)) m)) (theta (S m))) (le-theta-M-theta m) (monotonic-lt-times-l (theta (S m)) (lt-O-theta (S m)) (M m) (exp (S (S O)) (times (S (S O)) m)) (lt-M m posm))
let-clause-1033'''' : (n : nat) -> (lt1n : lt (S O) n) -> (x2515 : nat) -> (x2516 : nat) -> eq lzero nat x2515 (plus (times x2516 (div x2515 x2516)) (mod x2515 x2516))
let-clause-1033'''' = λ (n : nat) -> λ (lt1n : lt (S O) n) -> λ (x2515 : nat) -> λ (x2516 : nat) -> rewrite-l lzero lzero nat (times (div x2515 x2516) x2516) (λ (X-- : nat) -> eq lzero nat x2515 (plus X-- (mod x2515 x2516))) (div-mod x2515 x2516) (times x2516 (div x2515 x2516)) (commutative-times (div x2515 x2516) x2516)
theta-pred : (n : nat) -> (X-- : lt (S O) n) -> eq lzero nat (theta (times (S (S O)) n)) (theta (pred (times (S (S O)) n)))
theta-pred = λ (n : nat) -> λ (lt1n : lt (S O) n) -> eq-ind-r lzero lzero nat (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) -> eq lzero nat x (theta (pred (times (S (S O)) n)))) (eq-ind-r lzero lzero nat (bigop (S (pred (times (S (S O)) n))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (pred (times (S (S O)) n))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) -> eq lzero nat (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) x) (eq-ind-r lzero lzero nat (bigop (times (S (S O)) n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (times (S (S O)) n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i))) -> eq lzero nat x (bigop (S (pred (times (S (S O)) n))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (eq-ind-r lzero lzero nat (times (S (S O)) n) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) n)) -> eq lzero nat (bigop (times (S (S O)) n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop x (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X-- : nat) -> eq lzero nat (bigop X-- (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop (times (S (S O)) n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X-- : nat) -> eq lzero nat (bigop X-- (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop (times (S (S O)) n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero nat (bigop (plus n X--) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop (times (S (S O)) n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (bigop (plus n (plus n X--)) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop (times (S (S O)) n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (bigop (plus n X--) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop (times (S (S O)) n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X-- : nat) -> eq lzero nat (bigop (plus n n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop X-- (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X-- : nat) -> eq lzero nat (bigop (plus n n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop X-- (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero nat (bigop (plus n n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop (plus n X--) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (bigop (plus n n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop (plus n (plus n X--)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (bigop (plus n n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop (plus n X--) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) (refl lzero nat (bigop (plus n n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i))) (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)) (S (pred (times (S (S O)) n))) (S-pred (times (S (S O)) n) (eq-ind-r lzero lzero nat (times (S (S O)) O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) O)) -> lt x (times (S (S O)) n)) (monotonic-lt-times-r (S (S O)) (lt-to-le (S O) (S (S O)) (eq-coerc lzero (lt (mod (S O) O) (plus (plus (mod (S O) O) (times O (div (S O) O))) (S O))) (lt (S O) (S (S O))) (lt-plus-Sn-r (mod (S O) O) (times O (div (S O) O)) O) (rewrite-l lzero (lsuc lzero) nat (S O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (mod (S O) O) (plus X-- (S O))) (lt (S O) (S (S O)))) (rewrite-l lzero (lsuc lzero) nat (S O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (plus (S O) (S O))) (lt (S O) (S (S O)))) (rewrite-r lzero (lsuc lzero) nat (S (S O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (S O) X--) (lt (S O) (S (S O)))) (refl (lsuc lzero) (Set (lzero)) (lt (S O) (S (S O)))) (plus (S O) (S O)) (rewrite-r lzero lzero nat (times (S O) (S O)) (λ (X-- : nat) -> eq lzero nat (plus (S O) X--) (S (S O))) (rewrite-r lzero lzero nat (times (S (S O)) (S O)) (λ (X-- : nat) -> eq lzero nat (plus (S O) (times (S O) (S O))) X--) (times-Sn-m (S O) (S O)) (S (S O)) (times-n-1 (S (S O)))) (S O) (times-n-1 (S O)))) (mod (S O) O) (rewrite-r lzero lzero nat (plus O (mod (S O) O)) (λ (X-- : nat) -> eq lzero nat (S O) X--) (rewrite-l lzero lzero nat (plus (mod (S O) O) O) (λ (X-- : nat) -> eq lzero nat (S O) X--) (rewrite-r lzero lzero nat (times O (div (S O) O)) (λ (X-- : nat) -> eq lzero nat (S O) (plus (mod (S O) O) X--)) (rewrite-l lzero lzero nat (plus (times O (div (S O) O)) (mod (S O) O)) (λ (X-- : nat) -> eq lzero nat (S O) X--) (let-clause-1033'''' n lt1n (S O) O) (plus (mod (S O) O) (times O (div (S O) O))) (commutative-plus (times O (div (S O) O)) (mod (S O) O))) O (times-O-n (div (S O) O))) (plus O (mod (S O) O)) (commutative-plus (mod (S O) O) O)) (mod (S O) O) (plus-O-n (mod (S O) O)))) (plus (mod (S O) O) (times O (div (S O) O))) (rewrite-l lzero lzero nat (plus (times O (div (S O) O)) (mod (S O) O)) (λ (X-- : nat) -> eq lzero nat (S O) X--) (let-clause-1033'''' n lt1n (S O) O) (plus (mod (S O) O) (times O (div (S O) O))) (commutative-plus (times O (div (S O) O)) (mod (S O) O)))))) O n (lt-to-le (S O) n lt1n)) O (times-n-O (S (S O)))))) (bigop (S (times (S (S O)) n)) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> i)) (bigop-Sfalse (times (S (S O)) n) primeb nat (S O) times (λ (X-- : nat) -> X--) (not-prime-to-primeb-false (times (S (S O)) n) (nmk lzero (prime (times (S (S O)) n)) (λ (X-clearme : prime (times (S (S O)) n)) -> match-And lzero lzero (lt (S O) (times (S (S O)) n)) ((m : nat) -> (X-- : divides m (times (S (S O)) n)) -> (X--1 : lt (S O) m) -> eq lzero nat m (times (S (S O)) n)) lzero (λ (X-- : And lzero lzero (lt (S O) (times (S (S O)) n)) ((m : nat) -> (X-- : divides m (times (S (S O)) n)) -> (X--1 : lt (S O) m) -> eq lzero nat m (times (S (S O)) n))) -> False lzero) (λ (lt2n : lt (S O) (times (S (S O)) n)) -> λ (Hprime : (m : nat) -> (X-- : divides m (times (S (S O)) n)) -> (X--1 : lt (S O) m) -> eq lzero nat m (times (S (S O)) n)) -> absurd lzero (eq lzero nat (S (S O)) (times (S (S O)) n)) (Hprime (S (S O)) (quotient (S (S O)) (times (S (S O)) n) n (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X-- : nat) -> eq lzero nat X-- (times (S (S O)) n)) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X-- : nat) -> eq lzero nat X-- (times (S (S O)) n)) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero nat (plus n X--) (times (S (S O)) n)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (plus n (plus n X--)) (times (S (S O)) n)) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (plus n X--) (times (S (S O)) n)) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X-- : nat) -> eq lzero nat (plus n n) X--) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X-- : nat) -> eq lzero nat (plus n n) X--) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero nat (plus n n) (plus n X--)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (plus n n) (plus n (plus n X--))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (plus n n) (plus n X--)) (refl lzero nat (plus n 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)) (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))) (le-n (S (S O)))) (lt-to-not-eq (S (S O)) (times (S (S O)) n) (eq-ind-r lzero lzero nat (times (S (S O)) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) (S O))) -> lt x (times (S (S O)) n)) (monotonic-lt-times-r (S (S O)) (lt-O-S (S O)) (S O) n lt1n) (S (S O)) (times-n-1 (S (S O)))))) X-clearme))))) (theta (pred (times (S (S O)) n))) (theta-def (pred (times (S (S O)) n)))) (theta (times (S (S O)) n)) (theta-def (times (S (S O)) n))
le-theta : (m : nat) -> le (theta m) (exp (S (S O)) (times (S (S O)) m))
le-theta = λ (m : nat) -> nat-elim1 lzero m (λ (X-- : nat) -> le (theta X--) (exp (S (S O)) (times (S (S O)) X--))) (λ (m1 : nat) -> λ (Hind : (p : nat) -> (X-- : lt p m1) -> le (theta p) (exp (S (S O)) (times (S (S O)) p))) -> match-ex lzero lzero nat (λ (a : nat) -> Or lzero lzero (eq lzero nat m1 (times (S (S O)) a)) (eq lzero nat m1 (S (times (S (S O)) a)))) lzero (λ (X-- : ex lzero lzero nat (λ (a : nat) -> Or lzero lzero (eq lzero nat m1 (times (S (S O)) a)) (eq lzero nat m1 (S (times (S (S O)) a))))) -> le (theta m1) (exp (S (S O)) (times (S (S O)) m1))) (λ (a : nat) -> λ (X-clearme : Or lzero lzero (eq lzero nat m1 (times (S (S O)) a)) (eq lzero nat m1 (S (times (S (S O)) a)))) -> match-Or lzero lzero (eq lzero nat m1 (times (S (S O)) a)) (eq lzero nat m1 (S (times (S (S O)) a))) lzero (λ (X-- : Or lzero lzero (eq lzero nat m1 (times (S (S O)) a)) (eq lzero nat m1 (S (times (S (S O)) a)))) -> le (theta m1) (exp (S (S O)) (times (S (S O)) m1))) (λ (Ha : eq lzero nat m1 (times (S (S O)) a)) -> eq-ind-r lzero lzero nat (times (S (S O)) a) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) a)) -> le (theta x) (exp (S (S O)) (times (S (S O)) x))) (match-nat lzero (λ (X-- : nat) -> (X--1 : eq lzero nat m1 (times (S (S O)) X--)) -> le (theta (times (S (S O)) X--)) (exp (S (S O)) (times (S (S O)) (times (S (S O)) X--)))) (λ (X-- : eq lzero nat m1 (times (S (S O)) O)) -> le-n (theta (times (S (S O)) O))) (λ (n : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : eq lzero nat m1 (times (S (S O)) (S X--))) -> le (theta (times (S (S O)) (S X--))) (exp (S (S O)) (times (S (S O)) (times (S (S O)) (S X--))))) (λ (X-- : eq lzero nat m1 (times (S (S O)) (S O))) -> leb-true-to-le (theta (times (S (S O)) (S O))) (exp (S (S O)) (times (S (S O)) (times (S (S O)) (S O)))) (refl lzero bool (leb (theta (times (S (S O)) (S O))) (exp (S (S O)) (times (S (S O)) (times (S (S O)) (S O))))))) (λ (n1 : nat) -> λ (Hn1 : eq lzero nat m1 (times (S (S O)) (S (S n1)))) -> eq-ind-r lzero lzero nat (theta (pred (times (S (S O)) (S (S n1))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (theta (pred (times (S (S O)) (S (S n1)))))) -> le x (exp (S (S O)) (times (S (S O)) (times (S (S O)) (S (S n1)))))) (eq-ind-r lzero lzero nat (S (times (S (S O)) (S n1))) (λ (x : nat) -> λ (X-- : eq lzero nat x (S (times (S (S O)) (S n1)))) -> le (theta x) (exp (S (S O)) (times (S (S O)) (times (S (S O)) (S (S n1)))))) (transitive-le (theta (S (times (S (S O)) (S n1)))) (times (exp (S (S O)) (times (S (S O)) (S n1))) (theta (S (S n1)))) (exp (S (S O)) (times (S (S O)) (times (S (S O)) (S (S n1))))) (lt-to-le (theta (S (times (S (S O)) (S n1)))) (times (exp (S (S O)) (times (S (S O)) (S n1))) (theta (S (S n1)))) (lt-O-to-le-theta-exp-theta (S n1) (lt-O-S n1))) (eq-ind-r lzero lzero nat (plus (times (S (S O)) (S (S n1))) (times (S (S O)) (S (S n1)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (S (S O)) (S (S n1))) (times (S (S O)) (S (S n1))))) -> le (times (exp (S (S O)) (times (S (S O)) (S n1))) (theta (S (S n1)))) (exp (S (S O)) x)) (eq-ind-r lzero lzero nat (times (exp (S (S O)) (times (S (S O)) (S (S n1)))) (exp (S (S O)) (times (S (S O)) (S (S n1))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp (S (S O)) (times (S (S O)) (S (S n1)))) (exp (S (S O)) (times (S (S O)) (S (S n1)))))) -> le (times (exp (S (S O)) (times (S (S O)) (S n1))) (theta (S (S n1)))) x) (le-times (exp (S (S O)) (times (S (S O)) (S n1))) (exp (S (S O)) (times (S (S O)) (S (S n1)))) (theta (S (S n1))) (exp (S (S O)) (times (S (S O)) (S (S n1)))) (le-exp (times (S (S O)) (S n1)) (times (S (S O)) (S (S n1))) (S (S O)) (lt-O-S (S O)) (monotonic-le-times-r (S (S O)) (S n1) (S (S n1)) (le-n-Sn (S n1)))) (Hind (S (S n1)) (eq-ind-r lzero lzero nat (times (S (S O)) (S (S n1))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) (S (S n1)))) -> lt (S (S n1)) x) (eq-ind-r lzero lzero nat (plus (S (S n1)) (S (S n1))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S (S n1)) (S (S n1)))) -> lt (S (S n1)) x) (eq-coerc lzero (lt (S (S n1)) (plus (plus (S (S n1)) O) (S (S n1)))) (lt (S (S n1)) (plus (S (S n1)) (S (S n1)))) (lt-plus-Sn-r (S (S n1)) O (S n1)) (rewrite-r lzero (lsuc lzero) nat (plus (S (S n1)) (plus O (S (S n1)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (S (S n1)) X--) (lt (S (S n1)) (plus (S (S n1)) (S (S n1))))) (rewrite-l lzero (lsuc lzero) nat (S (S n1)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (S (S n1)) (plus (S (S n1)) X--)) (lt (S (S n1)) (plus (S (S n1)) (S (S n1))))) (refl (lsuc lzero) (Set (lzero)) (lt (S (S n1)) (plus (S (S n1)) (S (S n1))))) (plus O (S (S n1))) (plus-O-n (S (S n1)))) (plus (plus (S (S n1)) O) (S (S n1))) (associative-plus (S (S n1)) O (S (S n1))))) (times (S (S O)) (S (S n1))) (rewrite-r lzero lzero nat (times (S (S n1)) (S (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus (S (S n1)) (S (S n1)))) (rewrite-l lzero lzero nat (plus (S (S n1)) (times (S (S n1)) (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus (S (S n1)) (S (S n1)))) (rewrite-l lzero lzero nat (plus (S (S n1)) (times (S (S n1)) O)) (λ (X-- : nat) -> eq lzero nat (plus (S (S n1)) X--) (plus (S (S n1)) (S (S n1)))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (plus (S (S n1)) (plus (S (S n1)) X--)) (plus (S (S n1)) (S (S n1)))) (rewrite-l lzero lzero nat (S (S n1)) (λ (X-- : nat) -> eq lzero nat (plus (S (S n1)) X--) (plus (S (S n1)) (S (S n1)))) (refl lzero nat (plus (S (S n1)) (S (S n1)))) (plus (S (S n1)) O) (plus-n-O (S (S n1)))) (times (S (S n1)) O) (times-n-O (S (S n1)))) (times (S (S n1)) (S O)) (times-n-Sm (S (S n1)) O)) (times (S (S n1)) (S (S O))) (times-n-Sm (S (S n1)) (S O))) (times (S (S O)) (S (S n1))) (commutative-times (S (S O)) (S (S n1))))) m1 Hn1))) (exp (S (S O)) (plus (times (S (S O)) (S (S n1))) (times (S (S O)) (S (S n1))))) (exp-plus-times (S (S O)) (times (S (S O)) (S (S n1))) (times (S (S O)) (S (S n1))))) (times (S (S O)) (times (S (S O)) (S (S n1)))) (rewrite-r lzero lzero nat (times (times (S (S O)) (S (S n1))) (S (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus (times (S (S O)) (S (S n1))) (times (S (S O)) (S (S n1))))) (rewrite-l lzero lzero nat (plus (times (S (S O)) (S (S n1))) (times (times (S (S O)) (S (S n1))) (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus (times (S (S O)) (S (S n1))) (times (S (S O)) (S (S n1))))) (rewrite-l lzero lzero nat (plus (times (S (S O)) (S (S n1))) (times (times (S (S O)) (S (S n1))) O)) (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (S (S n1))) X--) (plus (times (S (S O)) (S (S n1))) (times (S (S O)) (S (S n1))))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (S (S n1))) (plus (times (S (S O)) (S (S n1))) X--)) (plus (times (S (S O)) (S (S n1))) (times (S (S O)) (S (S n1))))) (rewrite-l lzero lzero nat (times (S (S O)) (S (S n1))) (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (S (S n1))) X--) (plus (times (S (S O)) (S (S n1))) (times (S (S O)) (S (S n1))))) (refl lzero nat (plus (times (S (S O)) (S (S n1))) (times (S (S O)) (S (S n1))))) (plus (times (S (S O)) (S (S n1))) O) (plus-n-O (times (S (S O)) (S (S n1))))) (times (times (S (S O)) (S (S n1))) O) (times-n-O (times (S (S O)) (S (S n1))))) (times (times (S (S O)) (S (S n1))) (S O)) (times-n-Sm (times (S (S O)) (S (S n1))) O)) (times (times (S (S O)) (S (S n1))) (S (S O))) (times-n-Sm (times (S (S O)) (S (S n1))) (S O))) (times (S (S O)) (times (S (S O)) (S (S n1)))) (commutative-times (S (S O)) (times (S (S O)) (S (S n1))))))) (pred (times (S (S O)) (S (S n1)))) (eq-ind-r lzero lzero nat (plus n1 (S (S (plus n1 O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus n1 (S (S (plus n1 O))))) -> eq lzero nat (S (plus n1 (S (S (plus n1 O))))) (S x)) (rewrite-l lzero lzero nat n1 (λ (X-- : nat) -> eq lzero nat (S (plus n1 (S (S X--)))) (S (plus n1 (S (S (plus n1 O)))))) (rewrite-r lzero lzero nat (plus n1 (S (S (S n1)))) (λ (X-- : nat) -> eq lzero nat X-- (S (plus n1 (S (S (plus n1 O)))))) (rewrite-l lzero lzero nat n1 (λ (X-- : nat) -> eq lzero nat (plus n1 (S (S (S n1)))) (S (plus n1 (S (S X--))))) (rewrite-r lzero lzero nat (plus n1 (S (S (S n1)))) (λ (X-- : nat) -> eq lzero nat (plus n1 (S (S (S n1)))) X--) (refl lzero nat (plus n1 (S (S (S n1))))) (S (plus n1 (S (S n1)))) (plus-n-Sm n1 (S (S n1)))) (plus n1 O) (plus-n-O n1)) (S (plus n1 (S (S n1)))) (plus-n-Sm n1 (S (S n1)))) (plus n1 O) (plus-n-O n1)) (S (plus n1 (S (plus n1 O)))) (plus-n-Sm n1 (S (plus n1 O))))) (theta (times (S (S O)) (S (S n1)))) (theta-pred (S (S n1)) (le-S-S (S O) (S n1) (lt-O-S n1)))) n) a Ha) m1 Ha) (λ (Ha : eq lzero nat m1 (S (times (S (S O)) a))) -> eq-ind-r lzero lzero nat (S (times (S (S O)) a)) (λ (x : nat) -> λ (X-- : eq lzero nat x (S (times (S (S O)) a))) -> le (theta x) (exp (S (S O)) (times (S (S O)) x))) (match-nat lzero (λ (X-- : nat) -> (X--1 : eq lzero nat m1 (S (times (S (S O)) X--))) -> le (theta (S (times (S (S O)) X--))) (exp (S (S O)) (times (S (S O)) (S (times (S (S O)) X--))))) (λ (X-- : eq lzero nat m1 (S (times (S (S O)) O))) -> leb-true-to-le (theta (S (times (S (S O)) O))) (exp (S (S O)) (times (S (S O)) (S (times (S (S O)) O)))) (refl lzero bool (leb (theta (S (times (S (S O)) O))) (exp (S (S O)) (times (S (S O)) (S (times (S (S O)) O))))))) (λ (n : nat) -> λ (Hn : eq lzero nat m1 (S (times (S (S O)) (S n)))) -> transitive-le (theta (S (times (S (S O)) (S n)))) (times (exp (S (S O)) (times (S (S O)) (S n))) (theta (S (S n)))) (exp (S (S O)) (times (S (S O)) (S (times (S (S O)) (S n))))) (lt-to-le (theta (S (times (S (S O)) (S n)))) (times (exp (S (S O)) (times (S (S O)) (S n))) (theta (S (S n)))) (lt-O-to-le-theta-exp-theta (S n) (lt-O-S n))) (eq-ind-r lzero lzero nat (plus (S (times (S (S O)) (S n))) (S (times (S (S O)) (S n)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S (times (S (S O)) (S n))) (S (times (S (S O)) (S n))))) -> le (times (exp (S (S O)) (times (S (S O)) (S n))) (theta (S (S n)))) (exp (S (S O)) x)) (eq-ind lzero lzero nat (S (plus (S (times (S (S O)) (S n))) (times (S (S O)) (S n)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (plus (S (times (S (S O)) (S n))) (times (S (S O)) (S n)))) x-1) -> le (times (exp (S (S O)) (times (S (S O)) (S n))) (theta (S (S n)))) (exp (S (S O)) x-1)) (eq-ind lzero lzero nat (plus (times (S (S O)) (S n)) (S (times (S (S O)) (S n)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (times (S (S O)) (S n)) (S (times (S (S O)) (S n)))) x-1) -> le (times (exp (S (S O)) (times (S (S O)) (S n))) (theta (S (S n)))) (exp (S (S O)) (S x-1))) (eq-ind-r lzero lzero nat (plus (times (S (S O)) (S n)) (S (S (times (S (S O)) (S n))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (S (S O)) (S n)) (S (S (times (S (S O)) (S n)))))) -> le (times (exp (S (S O)) (times (S (S O)) (S n))) (theta (S (S n)))) (exp (S (S O)) x)) (eq-ind-r lzero lzero nat (times (exp (S (S O)) (times (S (S O)) (S n))) (exp (S (S O)) (S (S (times (S (S O)) (S n)))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp (S (S O)) (times (S (S O)) (S n))) (exp (S (S O)) (S (S (times (S (S O)) (S n))))))) -> le (times (exp (S (S O)) (times (S (S O)) (S n))) (theta (S (S n)))) x) (monotonic-le-times-r (exp (S (S O)) (times (S (S O)) (S n))) (theta (S (S n))) (exp (S (S O)) (S (S (times (S (S O)) (S n))))) (eq-ind lzero lzero nat (times (S (S O)) (S (S n))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (S (S O)) (S (S n))) x-1) -> le (theta (S (S n))) (exp (S (S O)) x-1)) (Hind (S (S n)) (eq-ind-r lzero lzero nat (S (times (S (S O)) (S n))) (λ (x : nat) -> λ (X-- : eq lzero nat x (S (times (S (S O)) (S n)))) -> lt (S (S n)) x) (le-S-S (S (S n)) (times (S (S O)) (S n)) (eq-ind-r lzero lzero nat (plus (S n) (S n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S n) (S n))) -> le (S (S n)) x) (eq-coerc lzero (le (S (S n)) (plus (S (S n)) n)) (le (S (S n)) (plus (S n) (S n))) (le-plus-n-r n (S (S n))) (rewrite-l lzero (lsuc lzero) nat (plus n (S (S n))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (S n)) X--) (le (S (S n)) (plus (S n) (S n)))) (rewrite-r lzero (lsuc lzero) nat (plus (S n) (S n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (S n)) X--) (le (S (S n)) (plus (S n) (S n)))) (refl (lsuc lzero) (Set (lzero)) (le (S (S n)) (plus (S n) (S n)))) (plus n (S (S n))) (rewrite-l lzero lzero nat (S (plus n (S n))) (λ (X-- : nat) -> eq lzero nat X-- (plus (S n) (S n))) (rewrite-l lzero lzero nat (plus (S n) n) (λ (X-- : nat) -> eq lzero nat (S X--) (plus (S n) (S n))) (plus-n-Sm (S n) n) (plus n (S n)) (commutative-plus (S n) n)) (plus n (S (S n))) (plus-n-Sm n (S n)))) (plus (S (S n)) n) (commutative-plus n (S (S n))))) (times (S (S O)) (S n)) (rewrite-r lzero lzero nat (times (S n) (S (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus (S n) (S n))) (rewrite-l lzero lzero nat (plus (S n) (times (S n) (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus (S n) (S n))) (rewrite-l lzero lzero nat (plus (S n) (times (S n) O)) (λ (X-- : nat) -> eq lzero nat (plus (S n) X--) (plus (S n) (S n))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (plus (S n) (plus (S n) X--)) (plus (S n) (S n))) (rewrite-l lzero lzero nat (S n) (λ (X-- : nat) -> eq lzero nat (plus (S n) X--) (plus (S n) (S n))) (refl lzero nat (plus (S n) (S n))) (plus (S n) O) (plus-n-O (S n))) (times (S n) O) (times-n-O (S n))) (times (S n) (S O)) (times-n-Sm (S n) O)) (times (S n) (S (S O))) (times-n-Sm (S n) (S O))) (times (S (S O)) (S n)) (commutative-times (S (S O)) (S n))))) m1 Hn)) (S (S (times (S (S O)) (S n)))) (eq-ind lzero lzero nat (S (plus (S n) (plus (S n) O))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (plus (S n) (plus (S n) O))) x-1) -> eq lzero nat (S x-1) (S (S (plus (S n) (plus (S n) O))))) (rewrite-l lzero lzero nat (S n) (λ (X-- : nat) -> eq lzero nat (S (S (plus (S n) X--))) (S (S (plus (S n) (plus (S n) O))))) (rewrite-r lzero lzero nat (plus (S n) (S (S n))) (λ (X-- : nat) -> eq lzero nat (S X--) (S (S (plus (S n) (plus (S n) O))))) (rewrite-r lzero lzero nat (plus (S n) (S (S (S n)))) (λ (X-- : nat) -> eq lzero nat X-- (S (S (plus (S n) (plus (S n) O))))) (rewrite-l lzero lzero nat (S n) (λ (X-- : nat) -> eq lzero nat (plus (S n) (S (S (S n)))) (S (S (plus (S n) X--)))) (rewrite-r lzero lzero nat (plus (S n) (S (S n))) (λ (X-- : nat) -> eq lzero nat (plus (S n) (S (S (S n)))) (S X--)) (rewrite-r lzero lzero nat (plus (S n) (S (S (S n)))) (λ (X-- : nat) -> eq lzero nat (plus (S n) (S (S (S n)))) X--) (refl lzero nat (plus (S n) (S (S (S n))))) (S (plus (S n) (S (S n)))) (plus-n-Sm (S n) (S (S n)))) (S (plus (S n) (S n))) (plus-n-Sm (S n) (S n))) (plus (S n) O) (plus-n-O (S n))) (S (plus (S n) (S (S n)))) (plus-n-Sm (S n) (S (S n)))) (S (plus (S n) (S n))) (plus-n-Sm (S n) (S n))) (plus (S n) O) (plus-n-O (S n))) (plus (S n) (S (plus (S n) O))) (plus-n-Sm (S n) (plus (S n) O))))) (exp (S (S O)) (plus (times (S (S O)) (S n)) (S (S (times (S (S O)) (S n)))))) (exp-plus-times (S (S O)) (times (S (S O)) (S n)) (S (S (times (S (S O)) (S n)))))) (S (plus (times (S (S O)) (S n)) (S (times (S (S O)) (S n))))) (plus-n-Sm (times (S (S O)) (S n)) (S (times (S (S O)) (S n))))) (plus (S (times (S (S O)) (S n))) (times (S (S O)) (S n))) (commutative-plus (times (S (S O)) (S n)) (S (times (S (S O)) (S n))))) (plus (S (times (S (S O)) (S n))) (S (times (S (S O)) (S n)))) (plus-n-Sm (S (times (S (S O)) (S n))) (times (S (S O)) (S n)))) (times (S (S O)) (S (times (S (S O)) (S n)))) (rewrite-r lzero lzero nat (times (S (times (S (S O)) (S n))) (S (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus (S (times (S (S O)) (S n))) (S (times (S (S O)) (S n))))) (rewrite-l lzero lzero nat (plus (S (times (S (S O)) (S n))) (times (S (times (S (S O)) (S n))) (S O))) (λ (X-- : nat) -> eq lzero nat X-- (plus (S (times (S (S O)) (S n))) (S (times (S (S O)) (S n))))) (rewrite-l lzero lzero nat (plus (S (times (S (S O)) (S n))) (times (S (times (S (S O)) (S n))) O)) (λ (X-- : nat) -> eq lzero nat (plus (S (times (S (S O)) (S n))) X--) (plus (S (times (S (S O)) (S n))) (S (times (S (S O)) (S n))))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (plus (S (times (S (S O)) (S n))) (plus (S (times (S (S O)) (S n))) X--)) (plus (S (times (S (S O)) (S n))) (S (times (S (S O)) (S n))))) (rewrite-l lzero lzero nat (S (times (S (S O)) (S n))) (λ (X-- : nat) -> eq lzero nat (plus (S (times (S (S O)) (S n))) X--) (plus (S (times (S (S O)) (S n))) (S (times (S (S O)) (S n))))) (refl lzero nat (plus (S (times (S (S O)) (S n))) (S (times (S (S O)) (S n))))) (plus (S (times (S (S O)) (S n))) O) (plus-n-O (S (times (S (S O)) (S n))))) (times (S (times (S (S O)) (S n))) O) (times-n-O (S (times (S (S O)) (S n))))) (times (S (times (S (S O)) (S n))) (S O)) (times-n-Sm (S (times (S (S O)) (S n))) O)) (times (S (times (S (S O)) (S n))) (S (S O))) (times-n-Sm (S (times (S (S O)) (S n))) (S O))) (times (S (S O)) (S (times (S (S O)) (S n)))) (commutative-times (S (S O)) (S (times (S (S O)) (S n))))))) a Ha) m1 Ha) X-clearme) (even-or-odd m1))