matita-arithmetics-chebyshev-bertrand.agda

open import Agda.Primitive
open import matita-arithmetics-factorial
open import matita-arithmetics-bigops
open import matita-arithmetics-sigma-pi
open import matita-arithmetics-primes
open import matita-arithmetics-chebyshev-chebyshev-psi
open import matita-arithmetics-chebyshev-chebyshev-theta
open import matita-arithmetics-chebyshev-factorization
open import matita-arithmetics-minimization
open import matita-arithmetics-chebyshev-psi-bounds
open import matita-arithmetics-sqrt
open import matita-arithmetics-log
open import matita-arithmetics-div-and-mod
open import matita-basics-logic
open import matita-basics-bool
open import matita-arithmetics-exp
open import matita-arithmetics-nat
bertrand : (X-n : nat) -> Set (lzero)
bertrand = λ (n : nat) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (le p (times (S (S O)) n))) (prime p))

not-bertrand : (X-n : nat) -> Set (lzero)
not-bertrand = λ (n : nat) -> (p : nat) -> (X-- : lt n p) -> (X--1 : le p (times (S (S O)) n)) -> Not lzero (prime p)

min-prim : (n : nat) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (prime p)) ((q : nat) -> (X-- : prime q) -> (X--1 : lt q p) -> le q n))
min-prim = λ (n : nat) -> match-Or lzero lzero (lt O n) (eq lzero nat O n) lzero (λ (X-- : Or lzero lzero (lt O n) (eq lzero nat O n)) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (prime p)) ((q : nat) -> (X--1 : prime q) -> (X--2 : lt q p) -> le q n))) (λ (Hn : lt O n) -> ex-intro lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (prime p)) ((q : nat) -> (X-- : prime q) -> (X--1 : lt q p) -> le q n)) (min' (S (fact n)) (S n) primeb) (conj lzero lzero (And lzero lzero (lt n (min' (S (fact n)) (S n) primeb)) (prime (min' (S (fact n)) (S n) primeb))) ((q : nat) -> (X-- : prime q) -> (X--1 : lt q (min' (S (fact n)) (S n) primeb)) -> le q n) (conj lzero lzero (lt n (min' (S (fact n)) (S n) primeb)) (prime (min' (S (fact n)) (S n) primeb)) (le-min-l primeb (S (fact n)) (S n)) (primeb-true-to-prime (min' (S (fact n)) (S n) primeb) (f-min-true primeb (S (fact n)) (S n) (match-ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt n m) (le m (S (fact n)))) (prime m)) lzero (λ (X-- : ex lzero lzero nat (λ (m : nat) -> And lzero lzero (And lzero lzero (lt n m) (le m (S (fact n)))) (prime m))) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le (S n) i) (lt i (plus (S (fact n)) (S n)))) (eq lzero bool (primeb i) true))) (λ (p : nat) -> λ (X-clearme : And lzero lzero (And lzero lzero (lt n p) (le p (S (fact n)))) (prime p)) -> match-And lzero lzero (And lzero lzero (lt n p) (le p (S (fact n)))) (prime p) lzero (λ (X-- : And lzero lzero (And lzero lzero (lt n p) (le p (S (fact n)))) (prime p)) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le (S n) i) (lt i (plus (S (fact n)) (S n)))) (eq lzero bool (primeb i) true))) (λ (X-clearme0 : And lzero lzero (lt n p) (le p (S (fact n)))) -> match-And lzero lzero (lt n p) (le p (S (fact n))) lzero (λ (X-- : And lzero lzero (lt n p) (le p (S (fact n)))) -> (X--1 : prime p) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le (S n) i) (lt i (plus (S (fact n)) (S n)))) (eq lzero bool (primeb i) true))) (λ (ltnp : lt n p) -> λ (lep : le p (S (fact n))) -> λ (primep : prime p) -> ex-intro lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le (S n) i) (lt i (plus (S (fact n)) (S n)))) (eq lzero bool (primeb i) true)) p (conj lzero lzero (And lzero lzero (le (S n) p) (lt p (plus (S (fact n)) (S n)))) (eq lzero bool (primeb p) true) (conj lzero lzero (le (S n) p) (lt p (plus (S (fact n)) (S n))) ltnp (eq-ind-r lzero lzero nat (plus p O) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus p O)) -> le (S x) (plus (S (fact n)) (S n))) (eq-ind-r lzero lzero nat (plus p (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus p (S O))) -> le x (plus (S (fact n)) (S n))) (le-plus p (S (fact n)) (S O) (S n) lep (lt-O-S n)) (S (plus p O)) (plus-n-Sm p O)) p (plus-n-O p))) (prime-to-primeb-true p primep))) X-clearme0) X-clearme) (ex-prime n Hn))))) (λ (p : nat) -> λ (primep : prime p) -> λ (ltp : lt p (min' (S (fact n)) (S n) primeb)) -> not-lt-to-le n p (nmk lzero (lt n p) (λ (ltnp : lt n p) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> (X--1 : eq lzero bool x false) -> False lzero) (λ (H : eq lzero bool true false) -> bool-discr lzero true false H (False lzero)) (primeb p) (prime-to-primeb-true p primep) (lt-min-to-false primeb (S (fact n)) p (S n) ltnp ltp)))))) (λ (Hn : eq lzero nat O n) -> ex-intro lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (prime p)) ((q : nat) -> (X-- : prime q) -> (X--1 : lt q p) -> le q n)) (S (S O)) (conj lzero lzero (And lzero lzero (lt n (S (S O))) (prime (S (S O)))) ((q : nat) -> (X-- : prime q) -> (X--1 : lt q (S (S O))) -> le q n) (conj lzero lzero (lt n (S (S O))) (prime (S (S O))) (eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> lt x-1 (S (S O))) (lt-O-S (S O)) n Hn) (primeb-true-to-prime (S (S O)) (refl lzero bool (primeb (S (S O)))))) (λ (p : nat) -> λ (primep : prime p) -> λ (lt2 : lt p (S (S O))) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> le p n) (absurd lzero (lt p (S (S O))) lt2 (le-to-not-lt (S (S O)) p (prime-to-lt-SO p primep)))))) (le-to-or-lt-eq O n (le-O-n n))

not-not-bertrand-to-bertrand1 : (n : nat) -> (X-- : Not lzero (not-bertrand n)) -> (x : nat) -> (X--1 : le n x) -> (X--2 : le x (times (S (S O)) n)) -> (X--3 : (p : nat) -> (X--3 : lt x p) -> (X--4 : le p (times (S (S O)) n)) -> Not lzero (prime p)) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (le p x)) (prime p))
not-not-bertrand-to-bertrand1 = λ (n : nat) -> λ (not-not : Not lzero (not-bertrand n)) -> λ (x : nat) -> λ (lenx : le n x) -> le-ind lzero n (λ (x-417 : nat) -> λ (X-x-418 : le n x-417) -> (X-- : le x-417 (times (S (S O)) n)) -> (X--1 : (p : nat) -> (X--1 : lt x-417 p) -> (X--2 : le p (times (S (S O)) n)) -> Not lzero (prime p)) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (le p x-417)) (prime p))) (λ (len : le n (times (S (S O)) n)) -> λ (Bn : (p : nat) -> (X-- : lt n p) -> (X--1 : le p (times (S (S O)) n)) -> Not lzero (prime p)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (le p n)) (prime p))) (absurd lzero (not-bertrand n) Bn not-not)) (λ (n1 : nat) -> λ (lenn1 : le n n1) -> λ (Hind : (X-- : le n1 (times (S (S O)) n)) -> (X--1 : (p : nat) -> (X--1 : lt n1 p) -> (X--2 : le p (times (S (S O)) n)) -> Not lzero (prime p)) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (le p n1)) (prime p))) -> λ (ltn1 : le (S n1) (times (S (S O)) n)) -> λ (HB : (p : nat) -> (X-- : lt (S n1) p) -> (X--1 : le p (times (S (S O)) n)) -> Not lzero (prime p)) -> 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)) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (le p (S n1))) (prime p))) (λ (Hc : eq lzero bool (primeb (S n1)) true) -> ex-intro lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (le p (S n1))) (prime p)) (S n1) (conj lzero lzero (And lzero lzero (lt n (S n1)) (le (S n1) (S n1))) (prime (S n1)) (conj lzero lzero (lt n (S n1)) (le (S n1) (S n1)) (le-S-S n n1 lenn1) (le-n (S n1))) (primeb-true-to-prime (S n1) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (primeb (S n1)) Hc)))) (λ (Hc : eq lzero bool (primeb (S n1)) false) -> match-ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (le p n1)) (prime p)) lzero (λ (X-- : ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (le p n1)) (prime p))) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (le p (S n1))) (prime p))) (λ (p : nat) -> λ (X-clearme : And lzero lzero (And lzero lzero (lt n p) (le p n1)) (prime p)) -> match-And lzero lzero (And lzero lzero (lt n p) (le p n1)) (prime p) lzero (λ (X-- : And lzero lzero (And lzero lzero (lt n p) (le p n1)) (prime p)) -> ex lzero lzero nat (λ (p0 : nat) -> And lzero lzero (And lzero lzero (lt n p0) (le p0 (S n1))) (prime p0))) (λ (X-clearme0 : And lzero lzero (lt n p) (le p n1)) -> match-And lzero lzero (lt n p) (le p n1) lzero (λ (X-- : And lzero lzero (lt n p) (le p n1)) -> (X--1 : prime p) -> ex lzero lzero nat (λ (p0 : nat) -> And lzero lzero (And lzero lzero (lt n p0) (le p0 (S n1))) (prime p0))) (λ (ltnp : lt n p) -> λ (lep : le p n1) -> λ (primep : prime p) -> ex-intro lzero lzero nat (λ (p0 : nat) -> And lzero lzero (And lzero lzero (lt n p0) (le p0 (S n1))) (prime p0)) p (conj lzero lzero (And lzero lzero (lt n p) (le p (S n1))) (prime p) (conj lzero lzero (lt n p) (le p (S n1)) ltnp (le-S p n1 lep)) primep)) X-clearme0) X-clearme) (Hind (lt-to-le n1 (times (S (S O)) n) ltn1) (λ (p : nat) -> λ (ltp : lt n1 p) -> λ (lep : le p (times (S (S O)) n)) -> match-Or lzero lzero (lt (S n1) p) (eq lzero nat (S n1) p) lzero (λ (X-- : Or lzero lzero (lt (S n1) p) (eq lzero nat (S n1) p)) -> Not lzero (prime p)) (λ (Hcase : lt (S n1) p) -> HB p Hcase lep) (λ (Hcase : eq lzero nat (S n1) p) -> eq-ind lzero lzero nat (S n1) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S n1) x-1) -> Not lzero (prime x-1)) (primeb-false-to-not-prime (S n1) (rewrite-r lzero lzero nat p (λ (X-- : nat) -> eq lzero bool (primeb X--) false) (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (primeb p) (rewrite-l lzero lzero nat (S n1) (λ (X-- : nat) -> eq lzero bool (primeb X--) false) Hc p Hcase)) (S n1) Hcase)) p Hcase) (le-to-or-lt-eq (S n1) p ltp)))) (true-or-false (primeb (S n1)))) x lenx

not-not-bertrand-to-bertrand : (n : nat) -> (X-- : Not lzero (not-bertrand n)) -> bertrand n
not-not-bertrand-to-bertrand = λ (n : nat) -> λ (not-not : Not lzero (not-bertrand n)) -> not-not-bertrand-to-bertrand1 n not-not (times (S (S O)) n) (le-plus-n-r (times (S O) n) n) (le-n (times (S (S O)) n)) (λ (p : nat) -> λ (le2n : lt (times (S (S O)) n) p) -> λ (lep : le p (times (S (S O)) n)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> Not lzero (prime p)) (absurd lzero (lt (times (S (S O)) n) p) le2n (le-to-not-lt p (times (S (S O)) n) lep)))

k : (X-n : nat) -> (X-p : nat) -> nat
k = λ (n : nat) -> λ (p : nat) -> bigop (log p n) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O)))

k-def : (n : nat) -> (p : nat) -> eq lzero nat (k n p) (bigop (log p n) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O))))
k-def = λ (n : nat) -> λ (p : nat) -> refl lzero nat (k n p)

le-k : (n : nat) -> (p : nat) -> le (k n p) (log p n)
le-k = λ (n : nat) -> λ (p : nat) -> eq-ind-r lzero lzero nat (bigop (log p n) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (log p n) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O))))) -> le x (log p n)) (nat-ind lzero (λ (X-x-365 : nat) -> le (bigop X-x-365 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O)))) X-x-365) (le-n (bigop O (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O))))) (λ (n1 : nat) -> λ (Hind : le (bigop n1 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O)))) n1) -> eq-ind-r lzero lzero nat (plus (mod (div n (exp p (S n1))) (S (S O))) (bigop n1 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (mod (div n (exp p (S n1))) (S (S O))) (bigop n1 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O)))))) -> le x (S n1)) (eq-ind-r lzero lzero nat (plus n1 O) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus n1 O)) -> le (plus (mod (div n (exp p (S n1))) (S (S O))) (bigop n1 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O))))) (S x)) (eq-ind-r lzero lzero nat (plus n1 (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus n1 (S O))) -> le (plus (mod (div n (exp p (S n1))) (S (S O))) (bigop n1 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O))))) x) (eq-ind-r lzero lzero nat (plus (bigop n1 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O)))) (mod (div n (exp p (S n1))) (S (S O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (bigop n1 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O)))) (mod (div n (exp p (S n1))) (S (S O))))) -> le x (plus n1 (S O))) (le-plus (bigop n1 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O)))) n1 (mod (div n (exp p (S n1))) (S (S O))) (S O) Hind (le-S-S-to-le (mod (div n (exp p (S n1))) (S (S O))) (S O) (lt-mod-m-m (div n (exp p (S n1))) (S (S O)) (lt-O-S (S O))))) (plus (mod (div n (exp p (S n1))) (S (S O))) (bigop n1 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O))))) (commutative-plus (mod (div n (exp p (S n1))) (S (S O))) (bigop n1 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O)))))) (S (plus n1 O)) (plus-n-Sm n1 O)) n1 (plus-n-O n1)) (bigop (S n1) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div n (exp p (S i))) (S (S O)))) (bigop-Strue n1 (λ (X-- : nat) -> true) nat O plus (λ (X-- : nat) -> mod (div n (exp p (S X--))) (S (S O))) (refl lzero bool true))) (log p n)) (k n p) (k-def n p)

Bk : (X-n : nat) -> nat
Bk = λ (n : nat) -> bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (k n p))

Bk-def : (n : nat) -> eq lzero nat (Bk n) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (k n p)))
Bk-def = λ (n : nat) -> refl lzero nat (Bk n)

Dexp : Dop lzero nat (S O)
Dexp = mk-Dop lzero nat (S O) timesAC (λ (a : nat) -> λ (b : nat) -> exp b a) (λ (a : nat) -> rewrite-l lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (refl lzero nat (S O)) (exp (S O) a) (exp-1-n a)) (λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> rewrite-r lzero lzero nat (exp (times b c) a) (λ (X-- : nat) -> eq lzero nat (exp (times b c) a) X--) (refl lzero nat (exp (times b c) a)) (times (exp b a) (exp c a)) (times-exp b c a))

eq-B-Bk : (n : nat) -> eq lzero nat (B n) (Bk n)
eq-B-Bk = λ (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 (mod (div n (exp p (S i))) (S (S O)))))) (λ (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 (mod (div n (exp p (S i))) (S (S O))))))) -> eq lzero nat x (Bk n)) (eq-ind-r lzero lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (k n p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (k n p)))) -> eq 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 (mod (div n (exp p (S i))) (S (S O)))))) x) (same-bigop (S n) primeb primeb nat (S O) times (λ (X-- : nat) -> bigop (log X-- n) (λ (i : nat) -> true) nat (S O) times (λ (i : nat) -> exp X-- (mod (div n (exp X-- (S i))) (S (S O))))) (λ (X-- : nat) -> exp X-- (k n X--)) (λ (i : nat) -> λ (auto : lt i (S n)) -> refl lzero bool (primeb i)) (λ (i : nat) -> λ (ltiS : lt i (S n)) -> λ (X-- : eq lzero bool (primeb i) true) -> eq-ind-r lzero lzero nat (bigop (log i n) (λ (i0 : nat) -> true) nat O plus (λ (i0 : nat) -> mod (div n (exp i (S i0))) (S (S O)))) (λ (x : nat) -> λ (X-0 : eq lzero nat x (bigop (log i n) (λ (i0 : nat) -> true) nat O plus (λ (i0 : nat) -> mod (div n (exp i (S i0))) (S (S O))))) -> eq lzero nat (bigop (log i n) (λ (i0 : nat) -> true) nat (S O) times (λ (i0 : nat) -> exp i (mod (div n (exp i (S i0))) (S (S O))))) (exp i x)) (exp-sigma-l (log i n) i (λ (X-0 : nat) -> true) (λ (X-0 : nat) -> mod (div n (exp i (S X-0))) (S (S O)))) (k n i) (k-def n i))) (Bk n) (Bk-def n)) (B n) (Bdef n)

B1 : (X-n : nat) -> nat
B1 = λ (n : nat) -> bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (k n p) (S O))) (k n p)))

B1-def : (n : nat) -> eq lzero nat (B1 n) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (k n p) (S O))) (k n p))))
B1-def = λ (n : nat) -> refl lzero nat (B1 n)

B2 : (X-n : nat) -> nat
B2 = λ (n : nat) -> bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (S (S O)) (k n p))) (k n p)))

B2-def : (n : nat) -> eq lzero nat (B2 n) (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (S (S O)) (k n p))) (k n p))))
B2-def = λ (n : nat) -> refl lzero nat (B2 n)

eq-Bk-B1-B2 : (n : nat) -> eq lzero nat (Bk n) (times (B1 n) (B2 n))
eq-Bk-B1-B2 = λ (n : nat) -> eq-ind-r lzero lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (k n p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (k n p)))) -> eq lzero nat x (times (B1 n) (B2 n))) (eq-ind-r lzero lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (k n p) (S O))) (k n p)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (k n p) (S O))) (k n p))))) -> eq lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (k n p))) (times x (B2 n))) (eq-ind-r lzero lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (S (S O)) (k n p))) (k n p)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (S (S O)) (k n p))) (k n p))))) -> eq lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (k n p))) (times (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (k n p) (S O))) (k n p)))) x)) (eq-ind lzero lzero nat (bigop (S n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> times (exp i (times (bool-to-nat (leb (k n i) (S O))) (k n i))) (exp i (times (bool-to-nat (leb (S (S O)) (k n i))) (k n i))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (bigop (S n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> times (exp i (times (bool-to-nat (leb (k n i) (S O))) (k n i))) (exp i (times (bool-to-nat (leb (S (S O)) (k n i))) (k n i))))) x-1) -> eq lzero nat (bigop (S n) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (k n p))) x-1) (same-bigop (S n) primeb primeb nat (S O) times (λ (X-- : nat) -> exp X-- (k n X--)) (λ (X-- : nat) -> times (exp X-- (times (bool-to-nat (leb (k n X--) (S O))) (k n X--))) (exp X-- (times (bool-to-nat (leb (S (S O)) (k n X--))) (k n X--)))) (λ (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) -> match-Or lzero lzero (eq lzero bool (leb (k n p) (S O)) true) (eq lzero bool (leb (k n p) (S O)) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (leb (k n p) (S O)) true) (eq lzero bool (leb (k n p) (S O)) false)) -> eq lzero nat (exp p (k n p)) (times (exp p (times (bool-to-nat (leb (k n p) (S O))) (k n p))) (exp p (times (bool-to-nat (leb (S (S O)) (k n p))) (k n p))))) (λ (Hc : eq lzero bool (leb (k n p) (S O)) true) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero nat (exp p (k n p)) (times (exp p (times (bool-to-nat x) (k n p))) (exp p (times (bool-to-nat (leb (S (S O)) (k n p))) (k n p))))) (eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero nat (exp p (k n p)) (times (exp p (times (bool-to-nat true) (k n p))) (exp p (times (bool-to-nat x) (k n p))))) (eq-ind lzero lzero nat (exp p (times (bool-to-nat true) (k n p))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp p (times (bool-to-nat true) (k n p))) x-1) -> eq lzero nat (exp p (k n p)) x-1) (eq-ind-r lzero lzero nat (times (k n p) (bool-to-nat true)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (k n p) (bool-to-nat true))) -> eq lzero nat (exp p (k n p)) (exp p x)) (eq-ind lzero lzero nat (k n p) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (k n p) x-1) -> eq lzero nat (exp p (k n p)) (exp p x-1)) (refl lzero nat (exp p (k n p))) (times (k n p) (S O)) (times-n-1 (k n p))) (times (bool-to-nat true) (k n p)) (commutative-times (bool-to-nat true) (k n p))) (times (exp p (times (bool-to-nat true) (k n p))) (S O)) (times-n-1 (exp p (times (bool-to-nat true) (k n p))))) (leb (S (S O)) (k n p)) (lt-to-leb-false (S (S O)) (k n p) (le-S-S (k n p) (S O) (leb-true-to-le (k n p) (S O) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (leb (k n p) (S O)) Hc))))) (leb (k n p) (S O)) Hc) (λ (Hc : eq lzero bool (leb (k n p) (S O)) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero nat (exp p (k n p)) (times (exp p (times (bool-to-nat x) (k n p))) (exp p (times (bool-to-nat (leb (S (S O)) (k n p))) (k n p))))) (eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero nat (exp p (k n p)) (times (exp p (times (bool-to-nat false) (k n p))) (exp p (times (bool-to-nat x) (k n p))))) (eq-ind-r lzero lzero nat (times (exp p (times (bool-to-nat true) (k n p))) (exp p (times (bool-to-nat false) (k n p)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p (times (bool-to-nat true) (k n p))) (exp p (times (bool-to-nat false) (k n p))))) -> eq lzero nat (exp p (k n p)) x) (eq-ind lzero lzero nat (exp p (times (bool-to-nat true) (k n p))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp p (times (bool-to-nat true) (k n p))) x-1) -> eq lzero nat (exp p (k n p)) x-1) (eq-ind-r lzero lzero nat (times (k n p) (bool-to-nat true)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (k n p) (bool-to-nat true))) -> eq lzero nat (exp p (k n p)) (exp p x)) (eq-ind lzero lzero nat (k n p) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (k n p) x-1) -> eq lzero nat (exp p (k n p)) (exp p x-1)) (refl lzero nat (exp p (k n p))) (times (k n p) (S O)) (times-n-1 (k n p))) (times (bool-to-nat true) (k n p)) (commutative-times (bool-to-nat true) (k n p))) (times (exp p (times (bool-to-nat true) (k n p))) (S O)) (times-n-1 (exp p (times (bool-to-nat true) (k n p))))) (times (exp p (times (bool-to-nat false) (k n p))) (exp p (times (bool-to-nat true) (k n p)))) (commutative-times (exp p (times (bool-to-nat false) (k n p))) (exp p (times (bool-to-nat true) (k n p))))) (leb (S (S O)) (k n p)) (le-to-leb-true (S (S O)) (k n p) (not-le-to-lt (k n p) (S O) (leb-false-to-not-le (k n p) (S O) (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (leb (k n p) (S O)) Hc))))) (leb (k n p) (S O)) Hc) (true-or-false (leb (k n p) (S O))))) (times (bigop (S n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (times (bool-to-nat (leb (k n i) (S O))) (k n i)))) (bigop (S n) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> exp i (times (bool-to-nat (leb (S (S O)) (k n i))) (k n i))))) (times-pi (S n) primeb (λ (X-- : nat) -> exp X-- (times (bool-to-nat (leb (k n X--) (S O))) (k n X--))) (λ (X-- : nat) -> exp X-- (times (bool-to-nat (leb (S (S O)) (k n X--))) (k n X--))))) (B2 n) (B2-def n)) (B1 n) (B1-def n)) (Bk n) (Bk-def n)

lt-div-to-times : (n : nat) -> (m : nat) -> (q : nat) -> (X-- : lt O q) -> (X--1 : lt (div n q) m) -> lt n (times q m)
lt-div-to-times = λ (n : nat) -> λ (m : nat) -> λ (q : nat) -> λ (posq : lt O q) -> λ (ltm : lt (div n q) m) -> not-le-to-lt (times q m) n (nmk lzero (le (times q m) n) (λ (len : le (times q m) n) -> absurd lzero (lt (div n q) m) ltm (le-to-not-lt m (div n q) (le-times-to-le-div n q m posq len))))

lt-to-div-O : (n : nat) -> (m : nat) -> (X-- : lt n m) -> eq lzero nat (div n m) O
lt-to-div-O = λ (n : nat) -> λ (m : nat) -> λ (ltnm : lt n m) -> div-mod-spec-to-eq n m (div n m) (mod n m) O n (div-mod-spec-div-mod n m (ltn-to-ltO n m ltnm)) (div-mod-spec-intro n m O n ltnm (rewrite-r lzero lzero nat (times m O) (λ (X-- : nat) -> eq lzero nat n (plus X-- n)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat n (plus X-- n)) (rewrite-r lzero lzero nat (plus n O) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) (plus n O) (plus-n-O n)) (plus O n) (commutative-plus O n)) (times m O) (times-n-O m)) (times O m) (commutative-times O m)))

k1 : (n : nat) -> (p : nat) -> (X-- : le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))) n) -> (X--1 : le p n) -> (X--2 : lt (div (times (S (S O)) n) (S (S (S O)))) p) -> eq lzero nat (k (times (S (S O)) n) p) O
k1 = λ (n : nat) -> λ (p : nat) -> λ (le18 : le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))) n) -> λ (lep : le p n) -> λ (ltp : lt (div (times (S (S O)) n) (S (S (S O)))) p) -> eq-ind-r lzero lzero nat (bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div (times (S (S O)) n) (exp p (S i))) (S (S O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (log p (times (S (S O)) n)) (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) -> eq lzero nat x O) (nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat (bigop X-x-365 (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div (times (S (S O)) n) (exp p (S i))) (S (S O)))) O) (refl lzero nat (bigop O (λ (i : nat) -> true) nat O plus (λ (i : nat) -> mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (λ (i : nat) -> λ (Hind : eq lzero nat (bigop i (λ (i0 : nat) -> true) nat O plus (λ (i0 : nat) -> mod (div (times (S (S O)) n) (exp p (S i0))) (S (S O)))) O) -> eq-ind-r lzero lzero nat (plus (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))) (bigop i (λ (i0 : nat) -> true) nat O plus (λ (i0 : nat) -> mod (div (times (S (S O)) n) (exp p (S i0))) (S (S O))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))) (bigop i (λ (i0 : nat) -> true) nat O plus (λ (i0 : nat) -> mod (div (times (S (S O)) n) (exp p (S i0))) (S (S O)))))) -> eq lzero nat x O) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (plus (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))) x) O) (eq-ind lzero lzero nat (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))) x-1) -> eq lzero nat x-1 O) (match-nat lzero (λ (X-- : nat) -> eq lzero nat (mod (div (times (S (S O)) n) (exp p (S X--))) (S (S O))) O) (eq-ind lzero lzero nat p (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat p x-1) -> eq lzero nat (mod (div (times (S (S O)) n) x-1) (S (S O))) O) (eq-ind-r lzero lzero nat (S (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (S (S O))) -> eq lzero nat (mod x (S (S O))) O) (refl lzero nat (mod (S (S O)) (S (S O)))) (div (times (S (S O)) n) p) (lt-to-le-times-to-lt-S-to-div (times (S (S O)) n) (S (S O)) p (ltn-to-ltO (div (times (S (S O)) n) (S (S (S O)))) p ltp) (eq-ind lzero lzero nat (times (S (S O)) p) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (S (S O)) p) x-1) -> le x-1 (times (S (S O)) n)) (monotonic-le-times-r (S (S O)) p n lep) (times p (S (S O))) (commutative-times (S (S O)) p)) (eq-ind-r lzero lzero nat (times (S (S (S O))) p) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S (S O))) p)) -> lt (times (S (S O)) n) x) (lt-div-to-times (times (S (S O)) n) p (S (S (S O))) (lt-O-S (S (S O))) ltp) (times p (S (S (S O)))) (commutative-times p (S (S (S O))))))) (exp p (S O)) (exp-n-1 p)) (λ (n2 : nat) -> eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (mod x (S (S O))) O) (rewrite-r lzero lzero nat O (λ (X-- : nat) -> eq lzero nat X-- O) (refl lzero nat O) (mod O (S (S O))) (mod-O-n (S (S O)))) (div (times (S (S O)) n) (exp p (S (S n2)))) (lt-to-div-O (times (S (S O)) n) (exp p (S (S n2))) (le-to-lt-to-lt (times (S (S O)) n) (exp (div (times (S (S O)) n) (S (S (S O)))) (S (S O))) (exp p (S (S n2))) (le-times-to-le (exp (S (S (S O))) (S (S O))) (times (S (S O)) n) (exp (div (times (S (S O)) n) (S (S (S O)))) (S (S O))) (leb-true-to-le (S O) (exp (S (S (S O))) (S (S O))) (refl lzero bool (leb (S O) (exp (S (S (S O))) (S (S O)))))) (eq-ind-r lzero lzero nat (times (exp (div (times (S (S O)) n) (S (S (S O)))) (S (S O))) (exp (S (S (S O))) (S (S O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp (div (times (S (S O)) n) (S (S (S O)))) (S (S O))) (exp (S (S (S O))) (S (S O))))) -> le (times (exp (S (S (S O))) (S (S O))) (times (S (S O)) n)) x) (eq-ind-r lzero lzero nat (exp (times (div (times (S (S O)) n) (S (S (S O)))) (S (S (S O)))) (S (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (exp (times (div (times (S (S O)) n) (S (S (S O)))) (S (S (S O)))) (S (S O)))) -> le (times (exp (S (S (S O))) (S (S O))) (times (S (S O)) n)) x) (transitive-le (times (exp (S (S (S O))) (S (S O))) (times (S (S O)) n)) (exp n (S (S O))) (exp (times (div (times (S (S O)) n) (S (S (S O)))) (S (S (S O)))) (S (S O))) (eq-ind lzero lzero nat (times (times (exp (S (S (S O))) (S (S O))) (S (S O))) n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (exp (S (S (S O))) (S (S O))) (S (S O))) n) x-1) -> le x-1 (exp n (S (S O)))) (eq-ind-r lzero lzero nat (times n n) (λ (x : nat) -> λ (X-- : eq lzero nat x (times n n)) -> le (times (times (exp (S (S (S O))) (S (S O))) (S (S O))) n) x) (le-times (times (exp (S (S (S O))) (S (S O))) (S (S O))) n n n le18 (le-n n)) (exp n (S (S O))) (exp-2 n)) (times (exp (S (S (S O))) (S (S O))) (times (S (S O)) n)) (associative-times (exp (S (S (S O))) (S (S O))) (S (S O)) n)) (le-exp1 n (times (div (times (S (S O)) n) (S (S (S O)))) (S (S (S O)))) (S (S O)) (lt-O-S (S O)) (le-plus-to-le (S (S (S O))) n (times (div (times (S (S O)) n) (S (S (S O)))) (S (S (S O)))) (eq-ind-r lzero lzero nat (times (S (div (times (S (S O)) n) (S (S (S O))))) (S (S (S O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (div (times (S (S O)) n) (S (S (S O))))) (S (S (S O))))) -> le (plus (S (S (S O))) n) x) (transitive-le (plus (S (S (S O))) n) (times (S (S O)) n) (times (S (div (times (S (S O)) n) (S (S (S O))))) (S (S (S O)))) (eq-ind lzero lzero nat n (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat n x-1) -> le (plus (S (S (S O))) n) (plus n x-1)) (monotonic-le-plus-l n (S (S (S O))) n (transitive-le (S (S (S O))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))) n (leb-true-to-le (S (S (S O))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))) (refl lzero bool (leb (S (S (S O))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))) le18)) (plus n O) (plus-n-O n)) (lt-to-le (times (S (S O)) n) (times (S (div (times (S (S O)) n) (S (S (S O))))) (S (S (S O)))) (lt-div-S (times (S (S O)) n) (S (S (S O))) (lt-O-S (S (S O)))))) (plus (S (S (S O))) (times (div (times (S (S O)) n) (S (S (S O)))) (S (S (S O))))) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (div X-- (S (S (S O)))) (S (S (S O))))) (times (S (div (times (S (S O)) n) (S (S (S O))))) (S (S (S O))))) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (div X-- (S (S (S O)))) (S (S (S O))))) (times (S (div (times (S (S O)) n) (S (S (S O))))) (S (S (S O))))) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (div (plus n X--) (S (S (S O)))) (S (S (S O))))) (times (S (div (times (S (S O)) n) (S (S (S O))))) (S (S (S O))))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (div (plus n (plus n X--)) (S (S (S O)))) (S (S (S O))))) (times (S (div (times (S (S O)) n) (S (S (S O))))) (S (S (S O))))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (div (plus n X--) (S (S (S O)))) (S (S (S O))))) (times (S (div (times (S (S O)) n) (S (S (S O))))) (S (S (S O))))) (rewrite-r lzero lzero nat (times (S (S (S O))) (div (plus n n) (S (S (S O))))) (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) X--) (times (S (div (times (S (S O)) n) (S (S (S O))))) (S (S (S O))))) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (S (S (S O))) (div (plus n n) (S (S (S O)))))) (times (S (div X-- (S (S (S O))))) (S (S (S O))))) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (S (S (S O))) (div (plus n n) (S (S (S O)))))) (times (S (div X-- (S (S (S O))))) (S (S (S O))))) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (S (S (S O))) (div (plus n n) (S (S (S O)))))) (times (S (div (plus n X--) (S (S (S O))))) (S (S (S O))))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (S (S (S O))) (div (plus n n) (S (S (S O)))))) (times (S (div (plus n (plus n X--)) (S (S (S O))))) (S (S (S O))))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (S (S (S O))) (div (plus n n) (S (S (S O)))))) (times (S (div (plus n X--) (S (S (S O))))) (S (S (S O))))) (rewrite-r lzero lzero nat (times (S (S (S O))) (S (div (plus n n) (S (S (S O)))))) (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (S (S (S O))) (div (plus n n) (S (S (S O)))))) X--) (rewrite-l lzero lzero nat (plus (S (S (S O))) (times (S (S (S O))) (div (plus n n) (S (S (S O)))))) (λ (X-- : nat) -> eq lzero nat (plus (S (S (S O))) (times (S (S (S O))) (div (plus n n) (S (S (S O)))))) X--) (refl lzero nat (plus (S (S (S O))) (times (S (S (S O))) (div (plus n n) (S (S (S O))))))) (times (S (S (S O))) (S (div (plus n n) (S (S (S O)))))) (times-n-Sm (S (S (S O))) (div (plus n n) (S (S (S O)))))) (times (S (div (plus n n) (S (S (S O))))) (S (S (S O)))) (commutative-times (S (div (plus n n) (S (S (S O))))) (S (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 (plus n n) (S (S (S O)))) (S (S (S O)))) (commutative-times (div (plus n n) (S (S (S O)))) (S (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 (exp (div (times (S (S O)) n) (S (S (S O)))) (S (S O))) (exp (S (S (S O))) (S (S O)))) (times-exp (div (times (S (S O)) n) (S (S (S O)))) (S (S (S O))) (S (S O)))) (times (exp (S (S (S O))) (S (S O))) (exp (div (times (S (S O)) n) (S (S (S O)))) (S (S O)))) (commutative-times (exp (S (S (S O))) (S (S O))) (exp (div (times (S (S O)) n) (S (S (S O)))) (S (S O)))))) (lt-to-le-to-lt (exp (div (times (S (S O)) n) (S (S (S O)))) (S (S O))) (exp p (S (S O))) (exp p (S (S n2))) (lt-exp1 (div (times (S (S O)) n) (S (S (S O)))) p (S (S O)) (lt-O-S (S O)) ltp) (le-exp (S (S O)) (S (S n2)) p (ltn-to-ltO (div (times (S (S O)) n) (S (S (S O)))) p ltp) (le-S-S (S O) (S n2) (le-S-S O n2 (le-O-n n2)))))))) i) (plus (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))) O) (plus-n-O (mod (div (times (S (S O)) n) (exp p (S i))) (S (S O))))) (bigop i (λ (i0 : nat) -> true) nat O plus (λ (i0 : nat) -> mod (div (times (S (S O)) n) (exp p (S i0))) (S (S O)))) Hind) (bigop (S i) (λ (i0 : nat) -> true) nat O plus (λ (i0 : nat) -> mod (div (times (S (S O)) n) (exp p (S i0))) (S (S O)))) (bigop-Strue i (λ (X-- : nat) -> true) nat O plus (λ (X-- : nat) -> mod (div (times (S (S O)) n) (exp p (S X--))) (S (S O))) (refl lzero bool true))) (log p (times (S (S O)) n))) (k (times (S (S O)) n) p) (k-def (times (S (S O)) n) p)

le-B1-theta : (n : nat) -> (X-- : le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))) n) -> (X--1 : not-bertrand n) -> le (B1 (times (S (S O)) n)) (theta (div (times (S (S O)) n) (S (S (S O)))))
le-B1-theta = λ (n : nat) -> λ (le18 : le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))) n) -> λ (not-Bn : not-bertrand n) -> eq-ind-r lzero lzero nat (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (k (times (S (S O)) n) p) (S O))) (k (times (S (S O)) n) 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) -> exp p (times (bool-to-nat (leb (k (times (S (S O)) n) p) (S O))) (k (times (S (S O)) n) p))))) -> le x (theta (div (times (S (S O)) n) (S (S (S O)))))) (eq-ind-r lzero lzero nat (bigop (S (div (times (S (S O)) n) (S (S (S O))))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (div (times (S (S O)) n) (S (S (S O))))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p))) -> le (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (k (times (S (S O)) n) p) (S O))) (k (times (S (S O)) n) p)))) x) (transitive-le (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (k (times (S (S O)) n) p) (S O))) (k (times (S (S O)) n) p)))) (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (bool-to-nat (eqb (k (times (S (S O)) n) p) (S O))))) (bigop (S (div (times (S (S O)) n) (S (S (S O))))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) (le-pi (S (times (S (S O)) n)) primeb (λ (X-- : nat) -> exp X-- (times (bool-to-nat (leb (k (times (S (S O)) n) X--) (S O))) (k (times (S (S O)) n) X--))) (λ (X-- : nat) -> exp X-- (bool-to-nat (eqb (k (times (S (S O)) n) X--) (S O)))) (λ (p : nat) -> λ (ltp : lt p (S (times (S (S O)) n))) -> λ (primebp : eq lzero bool (primeb p) true) -> le-exp (times (bool-to-nat (leb (k (times (S (S O)) n) p) (S O))) (k (times (S (S O)) n) p)) (bool-to-nat (eqb (k (times (S (S O)) n) p) (S O))) 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))) (match-Or lzero lzero (eq lzero bool (leb (k (times (S (S O)) n) p) (S O)) true) (eq lzero bool (leb (k (times (S (S O)) n) p) (S O)) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (leb (k (times (S (S O)) n) p) (S O)) true) (eq lzero bool (leb (k (times (S (S O)) n) p) (S O)) false)) -> le (times (bool-to-nat (leb (k (times (S (S O)) n) p) (S O))) (k (times (S (S O)) n) p)) (bool-to-nat (eqb (k (times (S (S O)) n) p) (S O)))) (λ (Hc : eq lzero bool (leb (k (times (S (S O)) n) p) (S O)) true) -> match-Or lzero lzero (lt (k (times (S (S O)) n) p) (S O)) (eq lzero nat (k (times (S (S O)) n) p) (S O)) lzero (λ (X-- : Or lzero lzero (lt (k (times (S (S O)) n) p) (S O)) (eq lzero nat (k (times (S (S O)) n) p) (S O))) -> le (times (bool-to-nat (leb (k (times (S (S O)) n) p) (S O))) (k (times (S (S O)) n) p)) (bool-to-nat (eqb (k (times (S (S O)) n) p) (S O)))) (λ (Hc0 : lt (k (times (S (S O)) n) p) (S O)) -> le-n-O-elim lzero (k (times (S (S O)) n) p) (le-S-S-to-le (k (times (S (S O)) n) p) O Hc0) (λ (X-- : nat) -> le (times (bool-to-nat (leb X-- (S O))) X--) (bool-to-nat (eqb X-- (S O)))) (eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> le x-1 (bool-to-nat (eqb O (S O)))) (le-n O) (times (bool-to-nat (leb O (S O))) O) (times-n-O (bool-to-nat (leb O (S O)))))) (λ (Hc0 : eq lzero nat (k (times (S (S O)) n) p) (S O)) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> le (times (bool-to-nat (leb (k (times (S (S O)) n) p) (S O))) (k (times (S (S O)) n) p)) (bool-to-nat x)) (eq-ind-r lzero lzero nat (S O) (λ (x : nat) -> λ (X-- : eq lzero nat x (S O)) -> le (times (bool-to-nat (leb x (S O))) x) (bool-to-nat true)) (le-n (times (bool-to-nat (leb (S O) (S O))) (S O))) (k (times (S (S O)) n) p) Hc0) (eqb (k (times (S (S O)) n) p) (S O)) (eq-to-eqb-true (k (times (S (S O)) n) p) (S O) Hc0)) (le-to-or-lt-eq (k (times (S (S O)) n) p) (S O) (leb-true-to-le (k (times (S (S O)) n) p) (S O) Hc))) (λ (Hc : eq lzero bool (leb (k (times (S (S O)) n) p) (S O)) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> le (times (bool-to-nat x) (k (times (S (S O)) n) p)) (bool-to-nat (eqb (k (times (S (S O)) n) p) (S O)))) (le-O-n (bool-to-nat (eqb (k (times (S (S O)) n) p) (S O)))) (leb (k (times (S (S O)) n) p) (S O)) Hc) (true-or-false (leb (k (times (S (S O)) n) p) (S O)))))) (transitive-le (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (bool-to-nat (eqb (k (times (S (S O)) n) p) (S O))))) (bigop (S (div (times (S (S O)) n) (S (S (S O))))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (bool-to-nat (eqb (k (times (S (S O)) n) p) (S O))))) (bigop (S (div (times (S (S O)) n) (S (S (S O))))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> p)) (eq-ind-r lzero lzero nat (bigop (S (times (S (S O)) n)) (λ (i : nat) -> primeb i) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> exp i (bool-to-nat (eqb (k (times (S (S O)) n) i) (S O))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (times (S (S O)) n)) (λ (i : nat) -> primeb i) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> exp i (bool-to-nat (eqb (k (times (S (S O)) n) i) (S O)))))) -> le (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (bool-to-nat (eqb (k (times (S (S O)) n) p) (S O))))) x) (le-n (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (bool-to-nat (eqb (k (times (S (S O)) n) p) (S O)))))) (bigop (S (div (times (S (S O)) n) (S (S (S O))))) (λ (i : nat) -> primeb i) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> exp i (bool-to-nat (eqb (k (times (S (S O)) n) i) (S O))))) (pad-bigop-nil (S (times (S (S O)) n)) (S (div (times (S (S O)) n) (S (S (S O))))) primeb nat (S O) timesA (λ (X-- : nat) -> exp X-- (bool-to-nat (eqb (k (times (S (S O)) n) X--) (S O)))) (le-S-S (div (times (S (S O)) n) (S (S (S O)))) (times (S (S O)) n) (le-times-to-le-div2 (times (S (S O)) n) (times (S (S O)) n) (S (S (S O))) (lt-O-S (S (S O))) (eq-ind-r lzero lzero nat (times (S (S (S O))) (times (S (S O)) n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S (S O))) (times (S (S O)) n))) -> le (times (S (S O)) n) x) (le-times (S (S O)) (S (S (S O))) n (times (S (S O)) n) (le-n-Sn (S (S O))) (le-plus-n-r (times (S O) n) n)) (times (times (S (S O)) n) (S (S (S O)))) (commutative-times (times (S (S O)) n) (S (S (S O))))))) (λ (i : nat) -> λ (lei : le (S (div (times (S (S O)) n) (S (S (S O))))) i) -> λ (lti : lt i (S (times (S (S O)) n))) -> match-Or lzero lzero (le (S n) i) (Not lzero (le (S n) i)) lzero (λ (X-- : Or lzero lzero (le (S n) i) (Not lzero (le (S n) i))) -> Or lzero lzero (eq lzero bool (primeb i) false) (eq lzero nat (exp i (bool-to-nat (eqb (k (times (S (S O)) n) i) (S O)))) (S O))) (λ (Hc : le (S n) i) -> or-introl lzero lzero (eq lzero bool (primeb i) false) (eq lzero nat (exp i (bool-to-nat (eqb (k (times (S (S O)) n) i) (S O)))) (S O)) (not-prime-to-primeb-false i (not-Bn i Hc (le-S-S-to-le i (times (S (S O)) n) lti)))) (λ (Hc : Not lzero (le (S n) i)) -> or-intror lzero lzero (eq lzero bool (primeb i) false) (eq lzero nat (exp i (bool-to-nat (eqb (k (times (S (S O)) n) i) (S O)))) (S O)) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (exp i (bool-to-nat (eqb x (S O)))) (S O)) (refl lzero nat (exp i (bool-to-nat (eqb O (S O))))) (k (times (S (S O)) n) i) (k1 n i le18 (not-lt-to-le n i Hc) lei))) (decidable-le (S n) i)))) (le-pi (S (div (times (S (S O)) n) (S (S (S O))))) primeb (λ (X-- : nat) -> exp X-- (bool-to-nat (eqb (k (times (S (S O)) n) X--) (S O)))) (λ (X-- : nat) -> X--) (λ (i : nat) -> λ (lti : lt i (S (div (times (S (S O)) n) (S (S (S O)))))) -> λ (primei : eq lzero bool (primeb i) true) -> match-bool lzero (λ (X-- : bool) -> le (exp i (bool-to-nat X--)) i) (eq-ind lzero lzero nat i (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat i x-1) -> le x-1 i) (le-n i) (exp i (S O)) (exp-n-1 i)) (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))) (eqb (k (times (S (S O)) n) i) (S O)))))) (theta (div (times (S (S O)) n) (S (S (S O))))) (theta-def (div (times (S (S O)) n) (S (S (S O)))))) (B1 (times (S (S O)) n)) (B1-def (times (S (S O)) n))

let-clause-1033''''''' : (n : nat) -> (len : le (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n) -> (p : nat) -> (lep : le (S (sqrt (times (S (S O)) n))) p) -> (ltp : lt p (S (times (S (S O)) n))) -> (Hc : eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) true) -> (H2n : lt (times (S (S O)) n) (exp p (S (S O)))) -> (x2515 : nat) -> (x2516 : nat) -> eq lzero nat x2515 (plus (times x2516 (div x2515 x2516)) (mod x2515 x2516))
let-clause-1033''''''' = λ (n : nat) -> λ (len : le (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n) -> λ (p : nat) -> λ (lep : le (S (sqrt (times (S (S O)) n))) p) -> λ (ltp : lt p (S (times (S (S O)) n))) -> λ (Hc : eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) true) -> λ (H2n : lt (times (S (S O)) n) (exp p (S (S O)))) -> λ (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)

le-B2-exp : (n : nat) -> (X-- : le (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n) -> le (B2 (times (S (S O)) n)) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O)))))
le-B2-exp = λ (n : nat) -> λ (len : le (exp (S (S O)) (S (S (S (S (S (S (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) -> exp p (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) 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) -> exp p (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p))))) -> le x (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O)))))) (transitive-le (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p)))) (bigop (S (sqrt (times (S (S O)) n))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p)))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O))))) (eq-ind-r lzero lzero nat (bigop (S (times (S (S O)) n)) (λ (i : nat) -> primeb i) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> exp i (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) i))) (k (times (S (S O)) n) i)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (bigop (S (times (S (S O)) n)) (λ (i : nat) -> primeb i) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> exp i (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) i))) (k (times (S (S O)) n) i))))) -> le (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p)))) x) (le-n (bigop (S (times (S (S O)) n)) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p))))) (bigop (S (sqrt (times (S (S O)) n))) (λ (i : nat) -> primeb i) nat (S O) (op lzero nat (S O) timesA) (λ (i : nat) -> exp i (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) i))) (k (times (S (S O)) n) i)))) (pad-bigop-nil (S (times (S (S O)) n)) (S (sqrt (times (S (S O)) n))) primeb nat (S O) timesA (λ (X-- : nat) -> exp X-- (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) X--))) (k (times (S (S O)) n) X--))) (le-S-S (sqrt (times (S (S O)) n)) (times (S (S O)) n) (le-sqrt-n (times (S (S O)) n))) (λ (p : nat) -> λ (lep : le (S (sqrt (times (S (S O)) n))) p) -> λ (ltp : lt p (S (times (S (S O)) n))) -> match-Or lzero lzero (eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) true) (eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) true) (eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) false)) -> Or lzero lzero (eq lzero bool (primeb p) false) (eq lzero nat (exp p (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p))) (S O))) (λ (Hc : eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) true) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> Or lzero lzero (eq lzero bool (primeb p) false) (eq lzero nat (exp p (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p))) (S O))) (absurd lzero (le p (sqrt (times (S (S O)) n))) (true-to-le-max (λ (x : nat) -> leb (times x x) (times (S (S O)) n)) (S (times (S (S O)) n)) p ltp (le-to-leb-true (times p p) (times (S (S O)) n) (eq-ind lzero lzero nat (exp p (S (S O))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp p (S (S O))) x-1) -> le x-1 (times (S (S O)) n)) (not-lt-to-le (times (S (S O)) n) (exp p (S (S O))) (nmk lzero (lt (times (S (S O)) n) (exp p (S (S O)))) (λ (H2n : lt (times (S (S O)) n) (exp p (S (S O)))) -> absurd lzero (lt (log p (times (S (S O)) n)) (S (S O))) (le-S-S (log p (times (S (S O)) n)) (S O) (f-false-to-le-max (λ (x : nat) -> leb (exp p x) (times (S (S O)) n)) (times (S (S O)) n) (S O) (ex-intro lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i (times (S (S O)) n)) (eq lzero bool (leb (exp p i) (times (S (S O)) n)) true)) O (conj lzero lzero (lt O (times (S (S O)) n)) (eq lzero bool (leb (exp p O) (times (S (S O)) n)) true) (eq-ind-r lzero lzero nat (times O (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O (S O))) -> lt x (times (S (S O)) n)) (eq-ind-r lzero lzero nat (times (S O) O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S O) O)) -> lt x (times (S (S O)) n)) (lt-times (S O) (S (S O)) O n (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 len p lep ltp Hc H2n (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 len p lep ltp Hc H2n (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))))) (lt-to-le-to-lt O (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n (leb-true-to-le (S O) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) (refl lzero bool (leb (S O) (exp (S (S O)) (S (S (S (S (S (S (S O))))))))))) len)) (times O (S O)) (commutative-times O (S O))) O (times-n-1 O)) (le-to-leb-true (exp p O) (times (S (S O)) n) (transitive-le (exp p O) n (times (S (S O)) n) (lt-to-le-to-lt O (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n (leb-true-to-le (S O) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) (refl lzero bool (leb (S O) (exp (S (S O)) (S (S (S (S (S (S (S O))))))))))) len) (le-plus-n-r (times (S O) n) n))))) (λ (m : nat) -> λ (lt1m : lt (S O) m) -> lt-to-leb-false (exp p m) (times (S (S O)) n) (lt-to-le-to-lt (times (S (S O)) n) (exp p (S (S O))) (exp p m) H2n (le-exp (S (S O)) m p (ltn-to-ltO (sqrt (times (S (S O)) n)) p lep) lt1m))))) (le-to-not-lt (S (S O)) (log p (times (S (S O)) n)) (transitive-le (S (S O)) (k (times (S (S O)) n) p) (log p (times (S (S O)) n)) (leb-true-to-le (S (S O)) (k (times (S (S O)) n) p) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X-- : nat) -> eq lzero bool (leb (S (S O)) (k X-- p)) true) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X-- : nat) -> eq lzero bool (leb (S (S O)) (k X-- p)) true) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero bool (leb (S (S O)) (k (plus n X--) p)) true) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero bool (leb (S (S O)) (k (plus n (plus n X--)) p)) true) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero bool (leb (S (S O)) (k (plus n X--) p)) true) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (leb (S (S O)) (k (plus n n) p)) (rewrite-r lzero lzero nat (plus n O) (λ (X-- : nat) -> eq lzero bool (leb (S (S O)) (k (plus n X--) p)) true) (rewrite-r lzero lzero nat (times n O) (λ (X-- : nat) -> eq lzero bool (leb (S (S O)) (k (plus n (plus n X--)) p)) true) (rewrite-r lzero lzero nat (times n (S O)) (λ (X-- : nat) -> eq lzero bool (leb (S (S O)) (k (plus n X--) p)) true) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X-- : nat) -> eq lzero bool (leb (S (S O)) (k X-- p)) true) (rewrite-l lzero lzero nat (times (S (S O)) n) (λ (X-- : nat) -> eq lzero bool (leb (S (S O)) (k X-- p)) true) Hc (times n (S (S O))) (commutative-times (S (S O)) n)) (plus n (times n (S O))) (times-n-Sm n (S O))) (plus n (times n O)) (times-n-Sm n O)) O (times-n-O n)) n (plus-n-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-k (times (S (S O)) n) p)))))) (times p p) (exp-2 p)))) (lt-to-not-le (sqrt (times (S (S O)) n)) p lep))) (λ (Hc : eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) false) -> or-intror lzero lzero (eq lzero bool (primeb p) false) (eq lzero nat (exp p (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p))) (S O)) (eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero nat (exp p (times (bool-to-nat x) (k (times (S (S O)) n) p))) (S O)) (refl lzero nat (exp p (times (bool-to-nat false) (k (times (S (S O)) n) p)))) (leb (S (S O)) (k (times (S (S O)) n) p)) Hc)) (true-or-false (leb (S (S O)) (k (times (S (S O)) n) p)))))) (transitive-le (bigop (S (sqrt (times (S (S O)) n))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> exp p (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p)))) (bigop (S (sqrt (times (S (S O)) n))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> times (S (S O)) n)) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O))))) (le-pi (S (sqrt (times (S (S O)) n))) primeb (λ (X-- : nat) -> exp X-- (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) X--))) (k (times (S (S O)) n) X--))) (λ (X-- : nat) -> times (S (S O)) n) (λ (p : nat) -> λ (ltp : lt p (S (sqrt (times (S (S O)) n)))) -> λ (primep : eq lzero bool (primeb p) true) -> transitive-le (exp p (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p))) (exp p (log p (times (S (S O)) n))) (times (S (S O)) n) (le-exp (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p)) (log p (times (S (S O)) n)) 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) primep))) (match-Or lzero lzero (eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) true) (eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) true) (eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) false)) -> le (times (bool-to-nat (leb (S (S O)) (k (times (S (S O)) n) p))) (k (times (S (S O)) n) p)) (log p (times (S (S O)) n))) (λ (Hc : eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) true) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> le (times (bool-to-nat x) (k (times (S (S O)) n) p)) (log p (times (S (S O)) n))) (eq-ind-r lzero lzero nat (times (k (times (S (S O)) n) p) (bool-to-nat true)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (k (times (S (S O)) n) p) (bool-to-nat true))) -> le x (log p (times (S (S O)) n))) (eq-ind lzero lzero nat (k (times (S (S O)) n) p) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (k (times (S (S O)) n) p) x-1) -> le x-1 (log p (times (S (S O)) n))) (le-k (times (S (S O)) n) p) (times (k (times (S (S O)) n) p) (S O)) (times-n-1 (k (times (S (S O)) n) p))) (times (bool-to-nat true) (k (times (S (S O)) n) p)) (commutative-times (bool-to-nat true) (k (times (S (S O)) n) p))) (leb (S (S O)) (k (times (S (S O)) n) p)) Hc) (λ (Hc : eq lzero bool (leb (S (S O)) (k (times (S (S O)) n) p)) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> le (times (bool-to-nat x) (k (times (S (S O)) n) p)) (log p (times (S (S O)) n))) (le-O-n (log p (times (S (S O)) n))) (leb (S (S O)) (k (times (S (S O)) n) p)) Hc) (true-or-false (leb (S (S O)) (k (times (S (S O)) n) p))))) (le-exp-log p (times (S (S O)) n) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> lt x (times (S (S O)) n)) (lt-times O (S (S O)) O n (lt-O-S (S O)) (lt-to-le-to-lt O (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n (leb-true-to-le (S O) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) (refl lzero bool (leb (S O) (exp (S (S O)) (S (S (S (S (S (S (S O))))))))))) len)) O (times-n-O O))))) (transitive-le (bigop (S (sqrt (times (S (S O)) n))) (λ (p : nat) -> primeb p) nat (S O) times (λ (p : nat) -> times (S (S O)) n)) (exp (times (S (S O)) n) (prim (sqrt (times (S (S O)) n)))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O))))) (eq-ind-r lzero lzero nat (exp (times (S (S O)) n) (bigop (S (sqrt (times (S (S O)) n))) (λ (i : nat) -> primeb i) nat O plus (λ (i : nat) -> S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (exp (times (S (S O)) n) (bigop (S (sqrt (times (S (S O)) n))) (λ (i : nat) -> primeb i) nat O plus (λ (i : nat) -> S O)))) -> le x (exp (times (S (S O)) n) (prim (sqrt (times (S (S O)) n))))) (le-n (exp (times (S (S O)) n) (bigop (S (sqrt (times (S (S O)) n))) (λ (i : nat) -> primeb i) nat O plus (λ (i : nat) -> S O)))) (bigop (S (sqrt (times (S (S O)) n))) (λ (i : nat) -> primeb i) nat (S O) times (λ (i : nat) -> times (S (S O)) n)) (exp-sigma (S (sqrt (times (S (S O)) n))) (times (S (S O)) n) primeb)) (le-exp (prim (sqrt (times (S (S O)) n))) (pred (div (sqrt (times (S (S O)) n)) (S (S O)))) (times (S (S O)) n) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> lt x (times (S (S O)) n)) (lt-times O (S (S O)) O n (lt-O-S (S O)) (lt-to-le-to-lt O (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n (leb-true-to-le (S O) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) (refl lzero bool (leb (S O) (exp (S (S O)) (S (S (S (S (S (S (S O))))))))))) len)) O (times-n-O O)) (le-prim-n3 (sqrt (times (S (S O)) n)) (true-to-le-max (λ (x : nat) -> leb (times x x) (times (S (S O)) n)) (S (times (S (S O)) n)) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))) (transitive-le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))) (times (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S O))))))))) (S (times (S (S O)) n)) (leb-true-to-le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))) (times (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))) (times (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))))))) (le-S (times (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S O))))))))) (times (S (S O)) n) (monotonic-le-times-r (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n len))) (le-to-leb-true (times (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))) (times (S (S O)) n) (transitive-le (times (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))) (times (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S O))))))))) (times (S (S O)) n) (leb-true-to-le (times (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))) (times (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (times (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))) (times (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))))))) (monotonic-le-times-r (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n len))))))))) (B2 (times (S (S O)) n)) (B2-def (times (S (S O)) n))

not-bertrand-to-le-B : (n : nat) -> (X-- : le (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n) -> (X--1 : not-bertrand n) -> le (B (times (S (S O)) n)) (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O))))))
not-bertrand-to-le-B = λ (n : nat) -> λ (len : le (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n) -> λ (notB : not-bertrand n) -> eq-ind-r lzero lzero nat (Bk (times (S (S O)) n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (Bk (times (S (S O)) n))) -> le x (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O))))))) (eq-ind-r lzero lzero nat (times (B1 (times (S (S O)) n)) (B2 (times (S (S O)) n))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (B1 (times (S (S O)) n)) (B2 (times (S (S O)) n)))) -> le x (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O))))))) (le-times (B1 (times (S (S O)) n)) (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (B2 (times (S (S O)) n)) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O))))) (transitive-le (B1 (times (S (S O)) n)) (theta (div (times (S (S O)) n) (S (S (S O))))) (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (le-B1-theta n (transitive-le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n (leb-true-to-le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))) (exp (S (S O)) (S (S (S (S (S (S (S O))))))))))) len) notB) (le-theta (div (times (S (S O)) n) (S (S (S O)))))) (le-B2-exp n len)) (Bk (times (S (S O)) n)) (eq-Bk-B1-B2 (times (S (S O)) n))) (B (times (S (S O)) n)) (eq-B-Bk (times (S (S O)) n))

le-times-div-m-m : (n : nat) -> (m : nat) -> (X-- : lt O m) -> le (times (div n m) m) n
le-times-div-m-m = λ (n : nat) -> λ (m : nat) -> λ (posm : lt O m) -> eq-ind-r lzero lzero nat (plus (times (div n m) m) (mod n m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (div n m) m) (mod n m))) -> le (times (div n m) m) x) (le-plus-n-r (mod n m) (times (div n m) m)) n (div-mod n m)

not-bertrand-to-le1 : (n : nat) -> (X-- : le (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n) -> (X--1 : not-bertrand n) -> le (exp (S (S O)) (div (times (S (S O)) n) (S (S (S O))))) (exp (times (S (S O)) n) (div (sqrt (times (S (S O)) n)) (S (S O))))
not-bertrand-to-le1 = λ (n : nat) -> λ (len : le (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n) -> λ (notB : not-bertrand n) -> le-times-to-le (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (S (S O)) (div (times (S (S O)) n) (S (S (S O))))) (exp (times (S (S O)) n) (div (sqrt (times (S (S O)) n)) (S (S O)))) (lt-O-exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O))))) (lt-O-S (S O))) (eq-ind lzero lzero nat (exp (S (S O)) (plus (times (S (S O)) (div (times (S (S O)) n) (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O)))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp (S (S O)) (plus (times (S (S O)) (div (times (S (S O)) n) (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O)))))) x-1) -> le x-1 (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (div (sqrt (times (S (S O)) n)) (S (S O)))))) (transitive-le (exp (S (S O)) (plus (times (S (S O)) (div (times (S (S O)) n) (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O)))))) (exp (S (S O)) (times (S (S O)) n)) (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (div (sqrt (times (S (S O)) n)) (S (S O))))) (le-exp (plus (times (S (S O)) (div (times (S (S O)) n) (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O))))) (times (S (S O)) n) (S (S O)) (lt-O-S (S O)) (eq-ind-r lzero lzero nat (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) -> le x (times (S (S O)) n)) (eq-ind-r lzero lzero nat (times (div (times (S (S O)) n) (S (S (S O)))) (S (S (S O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (div (times (S (S O)) n) (S (S (S O)))) (S (S (S O))))) -> le x (times (S (S O)) n)) (le-times-div-m-m (times (S (S O)) n) (S (S (S O))) (lt-O-S (S (S O)))) (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O))))) (commutative-times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (plus (times (S (S O)) (div (times (S (S O)) n) (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O))))) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (div X-- (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O))))) (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (div X-- (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O))))) (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (div (plus n X--) (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O))))) (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (div (plus n (plus n X--)) (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O))))) (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (div (plus n X--) (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O))))) (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (div (plus n n) (S (S (S O))))) (div X-- (S (S (S O))))) (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (div (plus n n) (S (S (S O))))) (div X-- (S (S (S O))))) (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (div (plus n n) (S (S (S O))))) (div (plus n X--) (S (S (S O))))) (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (div (plus n n) (S (S (S O))))) (div (plus n (plus n X--)) (S (S (S O))))) (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (plus (times (S (S O)) (div (plus n n) (S (S (S O))))) (div (plus n X--) (S (S (S O))))) (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-r lzero lzero nat (plus (div (plus n n) (S (S (S O)))) (times (S (S O)) (div (plus n n) (S (S (S O)))))) (λ (X-- : nat) -> eq lzero nat X-- (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-r lzero lzero nat (times (S (S (S O))) (div (plus n n) (S (S (S O))))) (λ (X-- : nat) -> eq lzero nat X-- (times (S (S (S O))) (div (times (S (S O)) n) (S (S (S O)))))) (rewrite-r lzero lzero nat (times n (S (S O))) (λ (X-- : nat) -> eq lzero nat (times (S (S (S O))) (div (plus n n) (S (S (S O))))) (times (S (S (S O))) (div X-- (S (S (S O)))))) (rewrite-l lzero lzero nat (plus n (times n (S O))) (λ (X-- : nat) -> eq lzero nat (times (S (S (S O))) (div (plus n n) (S (S (S O))))) (times (S (S (S O))) (div X-- (S (S (S O)))))) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero nat (times (S (S (S O))) (div (plus n n) (S (S (S O))))) (times (S (S (S O))) (div (plus n X--) (S (S (S O)))))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (times (S (S (S O))) (div (plus n n) (S (S (S O))))) (times (S (S (S O))) (div (plus n (plus n X--)) (S (S (S O)))))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (times (S (S (S O))) (div (plus n n) (S (S (S O))))) (times (S (S (S O))) (div (plus n X--) (S (S (S O)))))) (refl lzero nat (times (S (S (S O))) (div (plus n n) (S (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 (div (plus n n) (S (S (S O)))) (times (S (S O)) (div (plus n n) (S (S (S O)))))) (times-Sn-m (S (S O)) (div (plus n n) (S (S (S O)))))) (plus (times (S (S O)) (div (plus n n) (S (S (S O))))) (div (plus n n) (S (S (S O))))) (commutative-plus (times (S (S O)) (div (plus n n) (S (S (S O))))) (div (plus n n) (S (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)))) (transitive-le (exp (S (S O)) (times (S (S O)) n)) (times (times (S (S O)) n) (B (times (S (S O)) n))) (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (div (sqrt (times (S (S O)) n)) (S (S O))))) (le-exp-B n (transitive-le (S O) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n (leb-true-to-le (S O) (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) (refl lzero bool (leb (S O) (exp (S (S O)) (S (S (S (S (S (S (S O))))))))))) len)) (eq-ind lzero lzero nat (S (pred (div (sqrt (times (S (S O)) n)) (S (S O))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (pred (div (sqrt (times (S (S O)) n)) (S (S O))))) x-1) -> le (times (times (S (S O)) n) (B (times (S (S O)) n))) (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) x-1))) (eq-ind lzero lzero nat (times (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O)))))) (times (S (S O)) n)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O)))))) (times (S (S O)) n)) x-1) -> le (times (times (S (S O)) n) (B (times (S (S O)) n))) x-1) (eq-ind lzero lzero nat (times (times (S (S O)) n) (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O))))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (S (S O)) n) (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O))))))) x-1) -> le (times (times (S (S O)) n) (B (times (S (S O)) n))) x-1) (monotonic-le-times-r (times (S (S O)) n) (B (times (S (S O)) n)) (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O)))))) (not-bertrand-to-le-B n len notB)) (times (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O)))))) (times (S (S O)) n)) (commutative-times (times (S (S O)) n) (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O)))))))) (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (times (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O))))) (times (S (S O)) n))) (associative-times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (times (S (S O)) n) (pred (div (sqrt (times (S (S O)) n)) (S (S O))))) (times (S (S O)) n))) (div (sqrt (times (S (S O)) n)) (S (S O))) (S-pred (div (sqrt (times (S (S O)) n)) (S (S O))) (le-times-to-le-div (sqrt (times (S (S O)) n)) (S (S O)) (S O) (lt-O-S (S O)) (transitive-le (times (S (S O)) (S O)) (sqrt (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) (sqrt (times (S (S O)) n)) (leb-true-to-le (times (S (S O)) (S O)) (sqrt (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) (refl lzero bool (leb (times (S (S O)) (S O)) (sqrt (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))))))) (monotonic-sqrt (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (times (S (S O)) n) (eq-ind-r lzero lzero nat (times n (S (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times n (S (S O)))) -> le (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) x) (le-times (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n (S (S O)) (S (S O)) len (le-n (S (S O)))) (times (S (S O)) n) (commutative-times (S (S O)) n))))))))) (times (exp (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (exp-plus-times (S (S O)) (times (S (S O)) (div (times (S (S O)) n) (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O))))))

not-bertrand-to-le2 : (n : nat) -> (X-- : le (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n) -> (X--1 : not-bertrand n) -> le (div (times (S (S O)) n) (S (S (S O)))) (times (div (sqrt (times (S (S O)) n)) (S (S O))) (S (log (S (S O)) (times (S (S O)) n))))
not-bertrand-to-le2 = λ (n : nat) -> λ (len : le (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) n) -> λ (notB : not-bertrand n) -> eq-ind lzero lzero nat (log (S (S O)) (exp (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (log (S (S O)) (exp (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) x-1) -> le x-1 (times (div (sqrt (times (S (S O)) n)) (S (S O))) (S (log (S (S O)) (times (S (S O)) n))))) (transitive-le (log (S (S O)) (exp (S (S O)) (div (times (S (S O)) n) (S (S (S O)))))) (log (S (S O)) (exp (times (S (S O)) n) (div (sqrt (times (S (S O)) n)) (S (S O))))) (times (div (sqrt (times (S (S O)) n)) (S (S O))) (S (log (S (S O)) (times (S (S O)) n)))) (le-log (S (S O)) (exp (S (S O)) (div (times (S (S O)) n) (S (S (S O))))) (exp (times (S (S O)) n) (div (sqrt (times (S (S O)) n)) (S (S O)))) (le-n (S (S O))) (not-bertrand-to-le1 n len notB)) (log-exp1 (S (S O)) (times (S (S O)) n) (div (sqrt (times (S (S O)) n)) (S (S O))) (le-n (S (S O))))) (div (times (S (S O)) n) (S (S (S O)))) (eq-log-exp (S (S O)) (div (times (S (S O)) n) (S (S (S O)))) (le-n (S (S O))))

lt-div-S-div : (n : nat) -> (m : nat) -> (X-- : lt O m) -> (X--1 : le (exp m (S (S O))) n) -> lt (div n (S m)) (div n m)
lt-div-S-div = λ (n : nat) -> λ (m : nat) -> λ (posm : lt O m) -> λ (len : le (exp m (S (S O))) n) -> lt-times-to-lt-div (div n m) n (S m) (lt-to-le-to-lt n (times (S (div n m)) m) (times (div n m) (S m)) (lt-div-S n m posm) (eq-ind lzero lzero nat (plus (div n m) (times (div n m) m)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (div n m) (times (div n m) m)) x-1) -> le (times (S (div n m)) m) x-1) (eq-ind-r lzero lzero nat (times m (S (div n m))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times m (S (div n m)))) -> le x (plus (div n m) (times (div n m) m))) (eq-ind lzero lzero nat (plus m (times m (div n m))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus m (times m (div n m))) x-1) -> le x-1 (plus (div n m) (times (div n m) m))) (eq-ind-r lzero lzero nat (times (div n m) m) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (div n m) m)) -> le (plus m x) (plus (div n m) (times (div n m) m))) (le-plus m (div n m) (times (div n m) m) (times (div n m) m) (le-times-to-le-div n m m posm (eq-coerc lzero (le (exp m (S (S O))) n) (le (times m m) n) len (rewrite-r lzero (lsuc lzero) nat (times m m) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- n) (le (times m m) n)) (refl (lsuc lzero) (Set (lzero)) (le (times m m) n)) (exp m (S (S O))) (exp-2 m)))) (le-n (times (div n m) m))) (times m (div n m)) (commutative-times m (div n m))) (times m (S (div n m))) (times-n-Sm m (div n m))) (times (S (div n m)) m) (commutative-times (S (div n m)) m)) (times (div n m) (S m)) (times-n-Sm (div n m) m)))

times-div-le : (a : nat) -> (b : nat) -> (c : nat) -> (d : nat) -> (X-- : lt O b) -> (X--1 : lt O d) -> le (times (div a b) (div c d)) (div (times a c) (times b d))
times-div-le = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (d : nat) -> λ (posa : lt O b) -> λ (posb : lt O d) -> le-times-to-le-div (times a c) (times b d) (times (div a b) (div c d)) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> lt x (times b d)) (lt-times O b O d posa posb) O (times-n-O O)) (eq-ind-r lzero lzero nat (times (times (div a b) b) (times (div c d) d)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (times (div a b) b) (times (div c d) d))) -> le x (times a c)) (le-times (times (div a b) b) a (times (div c d) d) c (eq-coerc lzero (le (minus a (mod a b)) a) (le (times (div a b) b) a) (minus-le a (mod a b)) (rewrite-r lzero (lsuc lzero) nat (times b (div a b)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus a (mod a b)) a) (le X-- a)) (rewrite-l lzero (lsuc lzero) nat (times b (div a b)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- a) (le (times b (div a b)) a)) (refl (lsuc lzero) (Set (lzero)) (le (times b (div a b)) a)) (minus a (mod a b)) (rewrite-l lzero lzero nat (times (div a b) b) (λ (X-- : nat) -> eq lzero nat X-- (minus a (mod a b))) (eq-times-div-minus-mod a b) (times b (div a b)) (commutative-times (div a b) b))) (times (div a b) b) (commutative-times (div a b) b))) (eq-coerc lzero (le (minus c (mod c d)) c) (le (times (div c d) d) c) (minus-le c (mod c d)) (rewrite-r lzero (lsuc lzero) nat (times d (div c d)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus c (mod c d)) c) (le X-- c)) (rewrite-l lzero (lsuc lzero) nat (times d (div c d)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- c) (le (times d (div c d)) c)) (refl (lsuc lzero) (Set (lzero)) (le (times d (div c d)) c)) (minus c (mod c d)) (rewrite-l lzero lzero nat (times (div c d) d) (λ (X-- : nat) -> eq lzero nat X-- (minus c (mod c d))) (eq-times-div-minus-mod c d) (times d (div c d)) (commutative-times (div c d) d))) (times (div c d) d) (commutative-times (div c d) d)))) (times (times b d) (times (div a b) (div c d))) (rewrite-r lzero lzero nat (times b (times d (times (div a b) (div c d)))) (λ (X-- : nat) -> eq lzero nat X-- (times (times (div a b) b) (times (div c d) d))) (rewrite-r lzero lzero nat (times b (div a b)) (λ (X-- : nat) -> eq lzero nat (times b (times d (times (div a b) (div c d)))) (times X-- (times (div c d) d))) (rewrite-r lzero lzero nat (times d (div c d)) (λ (X-- : nat) -> eq lzero nat (times b (times d (times (div a b) (div c d)))) (times (times b (div a b)) X--)) (rewrite-r lzero lzero nat (times b (times (div a b) (times d (div c d)))) (λ (X-- : nat) -> eq lzero nat (times b (times d (times (div a b) (div c d)))) X--) (rewrite-r lzero lzero nat (times d (times (div a b) (div c d))) (λ (X-- : nat) -> eq lzero nat (times b (times d (times (div a b) (div c d)))) (times b X--)) (refl lzero nat (times b (times d (times (div a b) (div c d))))) (times (div a b) (times d (div c d))) (times-times (div a b) d (div c d))) (times (times b (div a b)) (times d (div c d))) (associative-times b (div a b) (times d (div c d)))) (times (div c d) d) (commutative-times (div c d) d)) (times (div a b) b) (commutative-times (div a b) b)) (times (times b d) (times (div a b) (div c d))) (associative-times b d (times (div a b) (div c d)))))

tech : (n : nat) -> (X-- : le (times (S (S O)) (S (log (S (S O)) (times (S (S O)) n)))) (sqrt (times (S (S O)) n))) -> le (times (div (sqrt (times (S (S O)) n)) (S (S O))) (S (log (S (S O)) (times (S (S O)) n)))) (div (times (S (S O)) n) (S (S (S (S O)))))
tech = λ (n : nat) -> λ (H : le (times (S (S O)) (S (log (S (S O)) (times (S (S O)) n)))) (sqrt (times (S (S O)) n))) -> eq-ind-r lzero lzero nat (times (S (log (S (S O)) (times (S (S O)) n))) (div (sqrt (times (S (S O)) n)) (S (S O)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (log (S (S O)) (times (S (S O)) n))) (div (sqrt (times (S (S O)) n)) (S (S O))))) -> le x (div (times (S (S O)) n) (S (S (S (S O)))))) (le-times-to-le-div (times (S (S O)) n) (S (S (S (S O)))) (times (S (log (S (S O)) (times (S (S O)) n))) (div (sqrt (times (S (S O)) n)) (S (S O)))) (lt-O-S (S (S (S O)))) (eq-ind lzero lzero nat (times (times (S (S (S (S O)))) (S (log (S (S O)) (times (S (S O)) n)))) (div (sqrt (times (S (S O)) n)) (S (S O)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (S (S (S (S O)))) (S (log (S (S O)) (times (S (S O)) n)))) (div (sqrt (times (S (S O)) n)) (S (S O)))) x-1) -> le x-1 (times (S (S O)) n)) (transitive-le (times (times (S (S (S (S O)))) (S (log (S (S O)) (times (S (S O)) n)))) (div (sqrt (times (S (S O)) n)) (S (S O)))) (times (times (S (S O)) (sqrt (times (S (S O)) n))) (div (sqrt (times (S (S O)) n)) (S (S O)))) (times (S (S O)) n) (le-times (times (S (S (S (S O)))) (S (log (S (S O)) (times (S (S O)) n)))) (times (S (S O)) (sqrt (times (S (S O)) n))) (div (sqrt (times (S (S O)) n)) (S (S O))) (div (sqrt (times (S (S O)) n)) (S (S O))) (eq-ind-r lzero lzero nat (times (S (S O)) (S (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) (S (S O)))) -> le (times x (S (log (S (S O)) (times (S (S O)) n)))) (times (S (S O)) (sqrt (times (S (S O)) n)))) (eq-ind-r lzero lzero nat (times (S (S O)) (times (S (S O)) (S (log (S (S O)) (times (S (S O)) n))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) (times (S (S O)) (S (log (S (S O)) (times (S (S O)) n)))))) -> le x (times (S (S O)) (sqrt (times (S (S O)) n)))) (monotonic-le-times-r (S (S O)) (times (S (S O)) (S (log (S (S O)) (times (S (S O)) n)))) (sqrt (times (S (S O)) n)) H) (times (times (S (S O)) (S (S O))) (S (log (S (S O)) (times (S (S O)) n)))) (associative-times (S (S O)) (S (S O)) (S (log (S (S O)) (times (S (S O)) n))))) (S (S (S (S O)))) (refl lzero nat (S (S (S (S O)))))) (le-n (div (sqrt (times (S (S O)) n)) (S (S O))))) (transitive-le (times (times (S (S O)) (sqrt (times (S (S O)) n))) (div (sqrt (times (S (S O)) n)) (S (S O)))) (div (times (times (S (S O)) (sqrt (times (S (S O)) n))) (sqrt (times (S (S O)) n))) (S (S O))) (times (S (S O)) n) (le-times-div-div-times (times (S (S O)) (sqrt (times (S (S O)) n))) (sqrt (times (S (S O)) n)) (S (S O)) (lt-O-S (S O))) (eq-ind-r lzero lzero nat (times (S (S O)) (times (sqrt (times (S (S O)) n)) (sqrt (times (S (S O)) n)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) (times (sqrt (times (S (S O)) n)) (sqrt (times (S (S O)) n))))) -> le (div x (S (S O))) (times (S (S O)) n)) (eq-ind-r lzero lzero nat (times (times (sqrt (times (S (S O)) n)) (sqrt (times (S (S O)) n))) (S (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (times (sqrt (times (S (S O)) n)) (sqrt (times (S (S O)) n))) (S (S O)))) -> le (div x (S (S O))) (times (S (S O)) n)) (eq-ind-r lzero lzero nat (times (sqrt (times (S (S O)) n)) (sqrt (times (S (S O)) n))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (sqrt (times (S (S O)) n)) (sqrt (times (S (S O)) n)))) -> le x (times (S (S O)) n)) (leq-sqrt-n (times (S (S O)) n)) (div (times (times (sqrt (times (S (S O)) n)) (sqrt (times (S (S O)) n))) (S (S O))) (S (S O))) (div-times (times (sqrt (times (S (S O)) n)) (sqrt (times (S (S O)) n))) (S (S O)) (lt-O-S (S O)))) (times (S (S O)) (times (sqrt (times (S (S O)) n)) (sqrt (times (S (S O)) n)))) (commutative-times (S (S O)) (times (sqrt (times (S (S O)) n)) (sqrt (times (S (S O)) n))))) (times (times (S (S O)) (sqrt (times (S (S O)) n))) (sqrt (times (S (S O)) n))) (associative-times (S (S O)) (sqrt (times (S (S O)) n)) (sqrt (times (S (S O)) n)))))) (times (S (S (S (S O)))) (times (S (log (S (S O)) (times (S (S O)) n))) (div (sqrt (times (S (S O)) n)) (S (S O))))) (associative-times (S (S (S (S O)))) (S (log (S (S O)) (times (S (S O)) n))) (div (sqrt (times (S (S O)) n)) (S (S O)))))) (times (div (sqrt (times (S (S O)) n)) (S (S O))) (S (log (S (S O)) (times (S (S O)) n)))) (commutative-times (div (sqrt (times (S (S O)) n)) (S (S O))) (S (log (S (S O)) (times (S (S O)) n))))

exp-to-log-r : (b : nat) -> (n : nat) -> (m : nat) -> (X-- : lt (S O) b) -> (X--1 : lt n m) -> (X--2 : le (exp b n) m) -> le n (log b m)
exp-to-log-r = λ (b : nat) -> λ (n : nat) -> λ (m : nat) -> λ (lt1b : lt (S O) b) -> λ (ltnm : lt n m) -> λ (Hexp : le (exp b n) m) -> true-to-le-max (λ (x : nat) -> leb (exp b x) m) m n ltnm (le-to-leb-true (exp b n) m Hexp)

let-clause-73'' : (n : nat) -> (posn : lt (S (S O)) n) -> (x134 : nat) -> (x135 : nat) -> (x136 : nat) -> eq lzero nat (plus x134 (plus x135 x136)) (plus x135 (plus x134 x136))
let-clause-73'' = λ (n : nat) -> λ (posn : lt (S (S O)) n) -> λ (x134 : nat) -> λ (x135 : nat) -> λ (x136 : nat) -> rewrite-l lzero lzero nat (plus (plus x135 x134) x136) (λ (X-- : nat) -> eq lzero nat (plus x134 (plus x135 x136)) X--) (assoc-plus1 x136 x135 x134) (plus x135 (plus x134 x136)) (associative-plus x135 x134 x136)

square-double : (n : nat) -> (X-- : lt (S (S O)) n) -> le (times (S n) (S n)) (times (times (S (S O)) n) n)
square-double = λ (n : nat) -> λ (posn : lt (S (S O)) n) -> eq-ind lzero lzero nat (plus n (times n n)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus n (times n n)) x-1) -> le (S (plus n x-1)) (times (plus n (plus n O)) n)) (eq-ind lzero lzero nat n (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat n x-1) -> le (S (plus n (plus n (times n n)))) (times (plus n x-1) n)) (eq-ind-r lzero lzero nat (plus (plus n (plus n (times n n))) O) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (plus n (plus n (times n n))) O)) -> le (S x) (times (plus n n) n)) (eq-ind-r lzero lzero nat (plus (times n n) (plus n (S n))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times n n) (plus n (S n)))) -> le x (times (plus n n) n)) (eq-ind-r lzero lzero nat (plus (times n n) (times n n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times n n) (times n n))) -> le (plus (times n n) (plus n (S n))) x) (monotonic-le-plus-r (times n n) (plus n (S n)) (times n n) (eq-ind lzero lzero nat (S (plus n n)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (plus n n)) x-1) -> le x-1 (times n n)) (eq-ind-r lzero lzero nat (times (S (S O)) n) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) n)) -> le (S x) (times n n)) (monotonic-lt-times-l n (ltn-to-ltO (S (S O)) n posn) (S (S O)) n posn) (plus n 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 (S n)) (plus-n-Sm n n))) (times (plus n n) n) (distributive-times-plus-r n n n)) (S (plus (plus n (plus n (times n n))) O)) (rewrite-r lzero lzero nat (plus O (plus n (plus n (times n n)))) (λ (X-- : nat) -> eq lzero nat (S X--) (plus (times n n) (plus n (S n)))) (rewrite-r lzero lzero nat (plus n (plus O (plus n (times n n)))) (λ (X-- : nat) -> eq lzero nat (S X--) (plus (times n n) (plus n (S n)))) (rewrite-r lzero lzero nat (plus n (plus O (times n n))) (λ (X-- : nat) -> eq lzero nat (S (plus n X--)) (plus (times n n) (plus n (S n)))) (rewrite-l lzero lzero nat (times n n) (λ (X-- : nat) -> eq lzero nat (S (plus n (plus n X--))) (plus (times n n) (plus n (S n)))) (rewrite-r lzero lzero nat (plus n (S (plus n (times n n)))) (λ (X-- : nat) -> eq lzero nat X-- (plus (times n n) (plus n (S n)))) (rewrite-r lzero lzero nat (plus n (S (times n n))) (λ (X-- : nat) -> eq lzero nat (plus n X--) (plus (times n n) (plus n (S n)))) (rewrite-r lzero lzero nat (plus n (plus (times n n) (S n))) (λ (X-- : nat) -> eq lzero nat (plus n (plus n (S (times n n)))) X--) (rewrite-r lzero lzero nat (plus n (plus (times n n) (S n))) (λ (X-- : nat) -> eq lzero nat X-- (plus n (plus (times n n) (S n)))) (refl lzero nat (plus n (plus (times n n) (S n)))) (plus n (plus n (S (times n n)))) (rewrite-l lzero lzero nat (S (plus (times n n) n)) (λ (X-- : nat) -> eq lzero nat (plus n (plus n (S (times n n)))) (plus n X--)) (rewrite-l lzero lzero nat (S (plus n (times n n))) (λ (X-- : nat) -> eq lzero nat (plus n X--) (plus n (S (plus (times n n) n)))) (rewrite-l lzero lzero nat (S (plus n (plus n (times n n)))) (λ (X-- : nat) -> eq lzero nat X-- (plus n (S (plus (times n n) n)))) (rewrite-l lzero lzero nat (plus n (plus (times n n) n)) (λ (X-- : nat) -> eq lzero nat (S X--) (plus n (S (plus (times n n) n)))) (plus-n-Sm n (plus (times n n) n)) (plus n (plus n (times n n))) (rewrite-l lzero lzero nat (plus (plus n n) (times n n)) (λ (X-- : nat) -> eq lzero nat (plus n (plus (times n n) n)) X--) (rewrite-l lzero lzero nat (plus (plus n (times n n)) n) (λ (X-- : nat) -> eq lzero nat X-- (plus (plus n n) (times n n))) (plus-plus-comm-23 n (times n n) n) (plus n (plus (times n n) n)) (associative-plus n (times n n) n)) (plus n (plus n (times n n))) (associative-plus n n (times n n)))) (plus n (S (plus n (times n n)))) (plus-n-Sm n (plus n (times n n)))) (plus n (S (times n n))) (plus-n-Sm n (times n n))) (plus (times n n) (S n)) (plus-n-Sm (times n n) n))) (plus (times n n) (plus n (S n))) (let-clause-73'' n posn (times n n) n (S n))) (S (plus n (times n n))) (plus-n-Sm n (times n n))) (S (plus n (plus n (times n n)))) (plus-n-Sm n (plus n (times n n)))) (plus O (times n n)) (plus-O-n (times n n))) (plus O (plus n (times n n))) (let-clause-73'' n posn O n (times n n))) (plus O (plus n (plus n (times n n)))) (let-clause-73'' n posn O n (plus n (times n n)))) (plus (plus n (plus n (times n n))) O) (commutative-plus (plus n (plus n (times n n))) O))) (plus n (plus n (times n n))) (plus-n-O (plus n (plus n (times n n))))) (plus n O) (plus-n-O n)) (times n (S n)) (times-n-Sm n n)

let-clause-10331'''' : (n : nat) -> (len : le (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) n) -> (m : nat) -> (lt2m : le (S (S (S O))) m) -> (Hind : le (plus (log (S (S O)) m) (S (S O))) m) -> (x2515 : nat) -> (x2516 : nat) -> eq lzero nat x2515 (plus (times x2516 (div x2515 x2516)) (mod x2515 x2516))
let-clause-10331'''' = λ (n : nat) -> λ (len : le (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) n) -> λ (m : nat) -> λ (lt2m : le (S (S (S O))) m) -> λ (Hind : le (plus (log (S (S O)) m) (S (S O))) m) -> λ (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)

sqrt-bound : (n : nat) -> (X-- : le (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) n) -> le (times (S (S O)) (S (log (S (S O)) (times (S (S O)) n)))) (sqrt (times (S (S O)) n))
sqrt-bound = λ (n : nat) -> λ (len : le (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) n) -> eq-ind-r lzero lzero nat (exp (S (S O)) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (exp (S (S O)) (S O))) -> le (times (S (S O)) (S (log (S (S O)) (times x n)))) (sqrt (times (S (S O)) n))) (eq-ind-r lzero lzero nat (plus (S O) (log (S (S O)) n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S O) (log (S (S O)) n))) -> le (times (S (S O)) (S x)) (sqrt (times (S (S O)) n))) (eq-ind-r lzero lzero nat (plus (log (S (S O)) n) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (log (S (S O)) n) (S O))) -> le (times (S (S O)) (S x)) (sqrt (times (S (S O)) n))) (eq-ind-r lzero lzero nat (plus (log (S (S O)) n) (S (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (log (S (S O)) n) (S (S O)))) -> le (times (S (S O)) x) (sqrt (times (S (S O)) n))) (true-to-le-max (λ (x : nat) -> leb (times x x) (times (S (S O)) n)) (S (times (S (S O)) n)) (times (S (S O)) (plus (log (S (S O)) n) (S (S O)))) (le-S-S (times (S (S O)) (plus (log (S (S O)) n) (S (S O)))) (times (S (S O)) n) (monotonic-le-times-r (S (S O)) (plus (log (S (S O)) n) (S (S O))) n (le-ind lzero (S (S (S O))) (λ (x-417 : nat) -> λ (X-x-418 : le (S (S (S O))) x-417) -> le (plus (log (S (S O)) x-417) (S (S O))) x-417) (le-n (plus (log (S (S O)) (S (S (S O)))) (S (S O)))) (λ (m : nat) -> λ (lt2m : le (S (S (S O))) m) -> λ (Hind : le (plus (log (S (S O)) m) (S (S O))) m) -> transitive-le (plus (log (S (S O)) (S m)) (S (S O))) (plus (log (S (S O)) (times (S (S O)) m)) (S (S O))) (S m) (le-plus (log (S (S O)) (S m)) (log (S (S O)) (times (S (S O)) m)) (S (S O)) (S (S O)) (le-log (S (S O)) (S m) (times (S (S O)) m) (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-10331'''' n len m lt2m Hind (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-10331'''' n len m lt2m Hind (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))))) (eq-ind lzero lzero nat m (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat m x-1) -> le (S m) (plus m x-1)) (eq-ind-r lzero lzero nat (plus m O) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus m O)) -> le (S x) (plus m m)) (eq-ind-r lzero lzero nat (plus m (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus m (S O))) -> le x (plus m m)) (monotonic-le-plus-r m (S O) m (transitive-le (S O) (S (S (S O))) m (leb-true-to-le (S O) (S (S (S O))) (refl lzero bool (leb (S O) (S (S (S O)))))) lt2m)) (S (plus m O)) (plus-n-Sm m O)) m (plus-n-O m)) (plus m O) (plus-n-O m))) (le-n (S (S O)))) (eq-ind-r lzero lzero nat (exp (S (S O)) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (exp (S (S O)) (S O))) -> le (plus (log (S (S O)) (times x m)) (S (S O))) (S m)) (eq-ind-r lzero lzero nat (plus (S O) (log (S (S O)) m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S O) (log (S (S O)) m))) -> le (plus x (S (S O))) (S m)) (le-S-S (plus (plus O (log (S (S O)) m)) (S (S O))) m Hind) (log (S (S O)) (times (exp (S (S O)) (S O)) m)) (log-exp (S (S O)) (S O) m (le-n (S (S O))) (transitive-le (S O) (S (S (S O))) m (leb-true-to-le (S O) (S (S (S O))) (refl lzero bool (leb (S O) (S (S (S O)))))) lt2m))) (S (S O)) (exp-n-1 (S (S O))))) n (lt-to-le-to-lt (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) n (le-S-S (S (S O)) (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times O (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (le-S-S (S O) (plus O (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times O (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (lt-O-S (plus (S O) (times (plus O (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times O (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O))))))) len)))) (le-to-leb-true (times (times (S (S O)) (plus (log (S (S O)) n) (S (S O)))) (times (S (S O)) (plus (log (S (S O)) n) (S (S O))))) (times (S (S O)) n) (eq-ind-r lzero lzero nat (times (S (S O)) (times (plus (log (S (S O)) n) (S (S O))) (times (S (S O)) (plus (log (S (S O)) n) (S (S O)))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) (times (plus (log (S (S O)) n) (S (S O))) (times (S (S O)) (plus (log (S (S O)) n) (S (S O))))))) -> le x (times (S (S O)) n)) (monotonic-le-times-r (S (S O)) (times (plus (log (S (S O)) n) (S (S O))) (times (S (S O)) (plus (log (S (S O)) n) (S (S O))))) n (eq-ind-r lzero lzero nat (plus (S (S O)) (log (S (S O)) n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S (S O)) (log (S (S O)) n))) -> le (times x (times (S (S O)) x)) n) (nat-elim1 lzero n (λ (X-- : nat) -> (X--1 : le (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) X--) -> le (times (plus (S (S O)) (log (S (S O)) X--)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) X--)))) X--) (λ (m : nat) -> λ (Hind : (p : nat) -> (X-- : lt p m) -> (X--1 : le (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) p) -> le (times (plus (S (S O)) (log (S (S O)) p)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) p)))) p) -> λ (lem : le (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m) -> match-Or lzero lzero (lt (exp (S (S O)) (log (S (S O)) m)) m) (eq lzero nat (exp (S (S O)) (log (S (S O)) m)) m) lzero (λ (X-- : Or lzero lzero (lt (exp (S (S O)) (log (S (S O)) m)) m) (eq lzero nat (exp (S (S O)) (log (S (S O)) m)) m)) -> le (times (plus (S (S O)) (log (S (S O)) m)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) m)))) m) (λ (Hclog : lt (exp (S (S O)) (log (S (S O)) m)) m) -> transitive-le (times (plus (S (S O)) (log (S (S O)) m)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) m)))) (exp (S (S O)) (log (S (S O)) m)) m (transitive-le (times (plus (S (S O)) (log (S (S O)) m)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) m)))) (times (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (log (S (S O)) m)))) (times (S (S O)) (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (log (S (S O)) m)))))) (exp (S (S O)) (log (S (S O)) m)) (eq-ind-r lzero lzero nat (log (S (S O)) m) (λ (x : nat) -> λ (X-- : eq lzero nat x (log (S (S O)) m)) -> le (times (plus (S (S O)) (log (S (S O)) m)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) m)))) (times (plus (S (S O)) x) (times (S (S O)) (plus (S (S O)) x)))) (le-n (times (plus (S (S O)) (log (S (S O)) m)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) m))))) (log (S (S O)) (exp (S (S O)) (log (S (S O)) m))) (eq-log-exp (S (S O)) (log (S (S O)) m) (le-n (S (S O))))) (Hind (exp (S (S O)) (log (S (S O)) m)) Hclog (le-exp (S (S (S (S (S (S (S (S O)))))))) (log (S (S O)) m) (S (S O)) (lt-O-S (S O)) (exp-to-log-r (S (S O)) (S (S (S (S (S (S (S (S O)))))))) m (le-n (S (S O))) (transitive-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) lem) lem)))) (le-exp-log (S (S O)) m (transitive-le (S O) (S (S O)) m (leb-true-to-le (S O) (S (S O)) (refl lzero bool (leb (S O) (S (S O))))) (transitive-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S O)) (S (S (S (S (S (S (S (S (S O)))))))))))) (transitive-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) lem))))) (λ (Hclog : eq lzero nat (exp (S (S O)) (log (S (S O)) m)) m) -> match-Or lzero lzero (lt (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m) (eq lzero nat (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m) lzero (λ (X-- : Or lzero lzero (lt (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m) (eq lzero nat (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m)) -> le (times (plus (S (S O)) (log (S (S O)) m)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) m)))) m) (λ (Hcasem : lt (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m) -> eq-ind lzero lzero nat (exp (S (S O)) (plus (minus (log (S (S O)) m) (S O)) (S O))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp (S (S O)) (plus (minus (log (S (S O)) m) (S O)) (S O))) x-1) -> (X-- : le (times (times (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))) (times (S (S O)) (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))))) (S (S O))) x-1) -> le (times (plus (S (S O)) (log (S (S O)) m)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) m)))) m) (eq-ind lzero lzero nat (log (S (S O)) m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (log (S (S O)) m) x-1) -> (X-- : le (times (times (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))) (times (S (S O)) (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))))) (S (S O))) (exp (S (S O)) x-1)) -> le (times (plus (S (S O)) (log (S (S O)) m)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) m)))) m) (λ (Hind0 : le (times (times (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))) (times (S (S O)) (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))))) (S (S O))) (exp (S (S O)) (log (S (S O)) m))) -> eq-ind lzero lzero nat (exp (S (S O)) (log (S (S O)) m)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp (S (S O)) (log (S (S O)) m)) x-1) -> le (times (plus (S (S O)) (log (S (S O)) x-1)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) x-1)))) x-1) (transitive-le (times (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (log (S (S O)) m)))) (times (S (S O)) (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (log (S (S O)) m)))))) (times (times (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))) (times (S (S O)) (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))))) (S (S O))) (exp (S (S O)) (log (S (S O)) m)) (eq-ind-r lzero lzero nat (log (S (S O)) m) (λ (x : nat) -> λ (X-- : eq lzero nat x (log (S (S O)) m)) -> le (times (plus (S (S O)) x) (times (S (S O)) (plus (S (S O)) x))) (times (times (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))) (times (S (S O)) (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))))) (S (S O)))) (eq-ind-r lzero lzero nat (minus (log (S (S O)) m) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (minus (log (S (S O)) m) (S O))) -> le (times (plus (S (S O)) (log (S (S O)) m)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) m)))) (times (times (plus (S (S O)) x) (times (S (S O)) (plus (S (S O)) x))) (S (S O)))) (eq-ind-r lzero lzero nat (minus (plus (S (S O)) (log (S (S O)) m)) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (minus (plus (S (S O)) (log (S (S O)) m)) (S O))) -> le (times (plus (S (S O)) (log (S (S O)) m)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) m)))) (times (times x (times (S (S O)) x)) (S (S O)))) (eq-ind-r lzero lzero nat (times (plus (S (S O)) (log (S (S O)) m)) (S (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (plus (S (S O)) (log (S (S O)) m)) (S (S O)))) -> le (times (plus (S (S O)) (log (S (S O)) m)) x) (times (times (minus (plus (S (S O)) (log (S (S O)) m)) (S O)) (times (S (S O)) (minus (plus (S (S O)) (log (S (S O)) m)) (S O)))) (S (S O)))) (eq-ind lzero lzero nat (times (times (plus (S (S O)) (log (S (S O)) m)) (plus (S (S O)) (log (S (S O)) m))) (S (S O))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (plus (S (S O)) (log (S (S O)) m)) (plus (S (S O)) (log (S (S O)) m))) (S (S O))) x-1) -> le x-1 (times (times (minus (plus (S (S O)) (log (S (S O)) m)) (S O)) (times (S (S O)) (minus (plus (S (S O)) (log (S (S O)) m)) (S O)))) (S (S O)))) (le-times (times (plus (S (S O)) (log (S (S O)) m)) (plus (S (S O)) (log (S (S O)) m))) (times (minus (plus (S (S O)) (log (S (S O)) m)) (S O)) (times (S (S O)) (minus (plus (S (S O)) (log (S (S O)) m)) (S O)))) (S (S O)) (S (S O)) (eq-ind lzero lzero nat (times (times (minus (plus (S (S O)) (log (S (S O)) m)) (S O)) (S (S O))) (minus (plus (S (S O)) (log (S (S O)) m)) (S O))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (minus (plus (S (S O)) (log (S (S O)) m)) (S O)) (S (S O))) (minus (plus (S (S O)) (log (S (S O)) m)) (S O))) x-1) -> le (times (plus (S (S O)) (log (S (S O)) m)) (plus (S (S O)) (log (S (S O)) m))) x-1) (eq-ind-r lzero lzero nat (times (S (S O)) (minus (plus (S (S O)) (log (S (S O)) m)) (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) (minus (plus (S (S O)) (log (S (S O)) m)) (S O)))) -> le (times (plus (S (S O)) (log (S (S O)) m)) (plus (S (S O)) (log (S (S O)) m))) (times x (minus (plus (S (S O)) (log (S (S O)) m)) (S O)))) (match-nat lzero (λ (X-- : nat) -> (X--1 : le (plus (S (S O)) (S (S (S O)))) X--) -> le (times X-- X--) (times (times (S (S O)) (minus X-- (S O))) (minus X-- (S O)))) (λ (auto : le (plus (S (S O)) (S (S (S O)))) O) -> le-x-times-x (times O O)) (λ (a0 : nat) -> λ (Hle : le (plus (S (S O)) (S (S (S O)))) (S a0)) -> eq-ind lzero lzero nat a0 (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat a0 x-1) -> le (times (S a0) (S a0)) (times (times (S (S O)) x-1) x-1)) (square-double a0 (le-S-S-to-le (S (S (S O))) a0 (lt-to-le (S (S (S (S O)))) (S a0) Hle))) (minus a0 O) (minus-n-O a0)) (plus (S (S O)) (log (S (S O)) m)) (monotonic-le-plus-r (S (S O)) (S (S (S O))) (log (S (S O)) m) (le-exp-to-le (S (S O)) (S (S (S O))) (log (S (S O)) m) (le-n (S (S O))) (eq-ind-r lzero lzero nat m (λ (x : nat) -> λ (X-- : eq lzero nat x m) -> le (exp (S (S O)) (S (S (S O)))) x) (lt-to-le (exp (S (S O)) (S (S (S O)))) m (transitive-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) lem)) (exp (S (S O)) (log (S (S O)) m)) Hclog)))) (times (minus (plus (S (S O)) (log (S (S O)) m)) (S O)) (S (S O))) (commutative-times (minus (plus (S (S O)) (log (S (S O)) m)) (S O)) (S (S O)))) (times (minus (plus (S (S O)) (log (S (S O)) m)) (S O)) (times (S (S O)) (minus (plus (S (S O)) (log (S (S O)) m)) (S O)))) (associative-times (minus (plus (S (S O)) (log (S (S O)) m)) (S O)) (S (S O)) (minus (plus (S (S O)) (log (S (S O)) m)) (S O)))) (le-n (S (S O)))) (times (plus (S (S O)) (log (S (S O)) m)) (times (plus (S (S O)) (log (S (S O)) m)) (S (S O)))) (associative-times (plus (S (S O)) (log (S (S O)) m)) (plus (S (S O)) (log (S (S O)) m)) (S (S O)))) (times (S (S O)) (plus (S (S O)) (log (S (S O)) m))) (commutative-times (S (S O)) (plus (S (S O)) (log (S (S O)) m)))) (plus (S (S O)) (minus (log (S (S O)) m) (S O))) (plus-minus-associative (S (S O)) (log (S (S O)) m) (S O) (lt-O-log (S (S O)) m (transitive-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S O)) (S (S (S (S (S (S (S (S (S O)))))))))))) (transitive-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) lem)) (transitive-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S O)) (S (S (S (S (S (S (S (S (S O)))))))))))) (transitive-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) lem))))) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O)))) (eq-log-exp (S (S O)) (minus (log (S (S O)) m) (S O)) (le-n (S (S O))))) (log (S (S O)) (exp (S (S O)) (log (S (S O)) m))) (eq-log-exp (S (S O)) (log (S (S O)) m) (le-n (S (S O))))) Hind0) m Hclog) (plus (minus (log (S (S O)) m) (S O)) (S O)) (plus-minus-m-m (log (S (S O)) m) (S O) (lt-O-log (S (S O)) m (transitive-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S O)) (S (S (S (S (S (S (S (S (S O)))))))))))) (transitive-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) lem)) (transitive-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S O)) (S (S (S (S (S (S (S (S (S O)))))))))))) (transitive-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) lem))))) (times (exp (S (S O)) (minus (log (S (S O)) m) (S O))) (S (S O))) (eq-ind lzero lzero nat (S (plus (minus (log (S (S O)) m) (S O)) O)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (plus (minus (log (S (S O)) m) (S O)) O)) x-1) -> eq lzero nat (exp (S (S O)) x-1) (times (exp (S (S O)) (minus (log (S (S O)) m) (S O))) (S (S O)))) (eq-ind lzero lzero nat (minus (log (S (S O)) m) (S O)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (minus (log (S (S O)) m) (S O)) x-1) -> eq lzero nat (exp (S (S O)) (S x-1)) (times (exp (S (S O)) (minus (log (S (S O)) m) (S O))) (S (S O)))) (rewrite-r lzero lzero nat (times (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O)))) (λ (X-- : nat) -> eq lzero nat X-- (times (exp (S (S O)) (minus (log (S (S O)) m) (S O))) (S (S O)))) (rewrite-r lzero lzero nat (times (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O)))) (λ (X-- : nat) -> eq lzero nat (times (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O)))) X--) (refl lzero nat (times (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))) (times (exp (S (S O)) (minus (log (S (S O)) m) (S O))) (S (S O))) (commutative-times (exp (S (S O)) (minus (log (S (S O)) m) (S O))) (S (S O)))) (exp (S (S O)) (S (minus (log (S (S O)) m) (S O)))) (exp-Sn (S (S O)) (minus (log (S (S O)) m) (S O)))) (plus (minus (log (S (S O)) m) (S O)) O) (plus-n-O (minus (log (S (S O)) m) (S O)))) (plus (minus (log (S (S O)) m) (S O)) (S O)) (plus-n-Sm (minus (log (S (S O)) m) (S O)) O)) (le-times (times (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))) (times (S (S O)) (plus (S (S O)) (log (S (S O)) (exp (S (S O)) (minus (log (S (S O)) m) (S O))))))) (exp (S (S O)) (minus (log (S (S O)) m) (S O))) (S (S O)) (S (S O)) (Hind (exp (S (S O)) (minus (log (S (S O)) m) (S O))) (eq-ind lzero lzero nat (exp (S (S O)) (log (S (S O)) m)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp (S (S O)) (log (S (S O)) m)) x-1) -> lt (exp (S (S O)) (minus (log (S (S O)) m) (S O))) x-1) (lt-exp (minus (log (S (S O)) m) (S O)) (log (S (S O)) m) (S (S O)) (le-n (S (S O))) (eq-ind-r lzero lzero nat (plus (minus (log (S (S O)) m) (S O)) O) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (minus (log (S (S O)) m) (S O)) O)) -> le (S x) (log (S (S O)) m)) (eq-ind-r lzero lzero nat (plus (minus (log (S (S O)) m) (S O)) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (minus (log (S (S O)) m) (S O)) (S O))) -> le x (log (S (S O)) m)) (eq-ind lzero lzero nat (log (S (S O)) m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (log (S (S O)) m) x-1) -> le x-1 (log (S (S O)) m)) (le-n (log (S (S O)) m)) (plus (minus (log (S (S O)) m) (S O)) (S O)) (plus-minus-m-m (log (S (S O)) m) (S O) (lt-O-log (S (S O)) m (transitive-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S O)) (S (S (S (S (S (S (S (S (S O)))))))))))) (transitive-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) lem)) (transitive-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S O)) (S (S (S (S (S (S (S (S (S O)))))))))))) (transitive-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) lem))))) (S (plus (minus (log (S (S O)) m) (S O)) O)) (plus-n-Sm (minus (log (S (S O)) m) (S O)) O)) (minus (log (S (S O)) m) (S O)) (plus-n-O (minus (log (S (S O)) m) (S O))))) m Hclog) (le-exp (S (S (S (S (S (S (S (S O)))))))) (minus (log (S (S O)) m) (S O)) (S (S O)) (lt-O-S (S O)) (le-plus-to-minus-r (S (S (S (S (S (S (S (S O)))))))) (S O) (log (S (S O)) m) (lt-exp-to-lt (S (S O)) (S (S (S (S (S (S (S (S O)))))))) (log (S (S O)) m) (lt-O-S (S O)) (eq-ind-r lzero lzero nat m (λ (x : nat) -> λ (X-- : eq lzero nat x m) -> lt (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) x) Hcasem (exp (S (S O)) (log (S (S O)) m)) Hclog))))) (le-n (S (S O))))) (λ (Hcasem : eq lzero nat (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m) -> eq-ind lzero lzero nat (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) x-1) -> le (times (plus (S (S O)) (log (S (S O)) x-1)) (times (S (S O)) (plus (S (S O)) (log (S (S O)) x-1)))) x-1) (eq-ind-r lzero lzero nat (S (S (S (S (S (S (S (S O)))))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (S (S (S (S (S (S (S (S O))))))))) -> le (times (plus (S (S O)) x) (times (S (S O)) (plus (S (S O)) x))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) (leb-true-to-le (times (plus (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (times (S (S O)) (plus (S (S O)) (S (S (S (S (S (S (S (S O))))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (times (plus (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (times (S (S O)) (plus (S (S O)) (S (S (S (S (S (S (S (S O))))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) (log (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) (eq-log-exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))) (le-n (S (S O))))) m Hcasem) (le-to-or-lt-eq (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m lem)) (le-to-or-lt-eq (exp (S (S O)) (log (S (S O)) m)) m (le-exp-log (S (S O)) m (transitive-le (S O) (S (S O)) m (leb-true-to-le (S O) (S (S O)) (refl lzero bool (leb (S O) (S (S O))))) (transitive-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S O)) (S (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S O)) (S (S (S (S (S (S (S (S (S O)))))))))))) (transitive-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) m (leb-true-to-le (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero bool (leb (S (S (S (S (S (S (S (S (S O))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) lem)))))) len) (plus (log (S (S O)) n) (S (S O))) (commutative-plus (log (S (S O)) n) (S (S O))))) (times (times (S (S O)) (plus (log (S (S O)) n) (S (S O)))) (times (S (S O)) (plus (log (S (S O)) n) (S (S O))))) (associative-times (S (S O)) (plus (log (S (S O)) n) (S (S O))) (times (S (S O)) (plus (log (S (S O)) n) (S (S O)))))))) (S (plus (log (S (S O)) n) (S O))) (plus-n-Sm (log (S (S O)) n) (S O))) (plus (S O) (log (S (S O)) n)) (commutative-plus (S O) (log (S (S O)) n))) (log (S (S O)) (times (exp (S (S O)) (S O)) n)) (log-exp (S (S O)) (S O) n (le-n (S (S O))) (lt-to-le-to-lt O (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) n (lt-O-S (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times O (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O))))) len))) (S (S O)) (exp-n-1 (S (S O)))

bertrand-up : (n : nat) -> (X-- : le (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) n) -> bertrand n
bertrand-up = λ (n : nat) -> λ (len : le (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) n) -> not-not-bertrand-to-bertrand n (nmk lzero (not-bertrand n) (λ (notBn : not-bertrand n) -> absurd lzero (le (div (times (S (S O)) n) (S (S (S O)))) (times (div (sqrt (times (S (S O)) n)) (S (S O))) (S (log (S (S O)) (times (S (S O)) n))))) (not-bertrand-to-le2 n (transitive-le (exp (S (S O)) (S (S (S (S (S (S (S O)))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) n (le-exp (S (S (S (S (S (S (S O))))))) (S (S (S (S (S (S (S (S O)))))))) (S (S O)) (lt-O-S (S O)) (le-n-Sn (S (S (S (S (S (S (S O))))))))) len) notBn) (lt-to-not-le (times (div (sqrt (times (S (S O)) n)) (S (S O))) (S (log (S (S O)) (times (S (S O)) n)))) (div (times (S (S O)) n) (S (S (S O)))) (le-to-lt-to-lt (times (div (sqrt (times (S (S O)) n)) (S (S O))) (S (log (S (S O)) (times (S (S O)) n)))) (div (times (S (S O)) n) (S (S (S (S O))))) (div (times (S (S O)) n) (S (S (S O)))) (tech n (sqrt-bound n len)) (lt-div-S-div (times (S (S O)) n) (S (S (S O))) (lt-O-S (S (S O))) (transitive-le (exp (S (S (S O))) (S (S O))) (times (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) (times (S (S O)) n) (leb-true-to-le (exp (S (S (S O))) (S (S O))) (times (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) (refl lzero bool (leb (exp (S (S (S O))) (S (S O))) (times (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))))))) (monotonic-le-times-r (S (S O)) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) n len)))))))