matita-arithmetics-log.agda

open import Agda.Primitive
open import matita-arithmetics-minimization
open import matita-basics-bool
open import matita-arithmetics-div-and-mod
open import matita-basics-logic
open import matita-arithmetics-exp
open import matita-arithmetics-nat
log : (X-p : nat) -> (X-n : nat) -> nat
log = λ (p : nat) -> λ (n : nat) -> max'' n (λ (x : nat) -> leb (exp p x) n)

tech-log : (p : nat) -> (n : nat) -> (X-- : lt (S O) p) -> (X--1 : lt O n) -> eq lzero nat (log p n) (max'' (S n) (λ (x : nat) -> leb (exp p x) n))
tech-log = λ (p : nat) -> λ (n : nat) -> λ (lt1p : lt (S O) p) -> λ (posn : lt O n) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero nat (log p n) (match-bool lzero (λ (X-0 : bool) -> nat) n (max' n (λ (x0 : nat) -> leb (exp p x0) n) O) x)) (refl lzero nat (log p n)) (leb (exp p n) n) (not-le-to-leb-false (exp p n) n (lt-to-not-le n (exp p n) (lt-m-exp-nm p n lt1p)))

le-exp-log : (p : nat) -> (n : nat) -> (X-- : lt O n) -> le (exp p (log p n)) n
le-exp-log = λ (a : nat) -> λ (n : nat) -> λ (posn : lt O n) -> leb-true-to-le (exp a (log a n)) n (f-max-true (λ (x : nat) -> leb (exp a x) n) n (ex-intro lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i n) (eq lzero bool (leb (exp a i) n) true)) O (conj lzero lzero (lt O n) (eq lzero bool (leb (exp a O) n) true) posn (le-to-leb-true (exp a O) n posn))))

log-SO : (n : nat) -> (X-- : lt (S O) n) -> eq lzero nat (log n (S O)) O
log-SO = λ (n : nat) -> λ (lt1n : lt (S O) n) -> sym-eq lzero nat O (log n (S O)) (le-n-O-to-eq (log n (S O)) (le-exp-to-le n (log n (S O)) O lt1n (le-n (exp n (log n (S O))))))

lt-to-log-O : (n : nat) -> (m : nat) -> (X-- : lt O m) -> (X--1 : lt m n) -> eq lzero nat (log n m) O
lt-to-log-O = λ (n : nat) -> λ (m : nat) -> λ (posm : lt O m) -> λ (ltnm : lt m n) -> sym-eq lzero nat O (log n m) (le-n-O-to-eq (log n m) (le-S-S-to-le (log n m) O (lt-exp-to-lt n (log n m) (S O) (le-to-lt-to-lt O m n (le-O-n m) ltnm) (eq-ind lzero lzero nat n (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat n x-1) -> lt (exp n (log n m)) x-1) (le-to-lt-to-lt (exp n (log n m)) m n (le-exp-log n m posm) ltnm) (plus n O) (plus-n-O n)))))

lt-log-n-n : (p : nat) -> (n : nat) -> (X-- : lt (S O) p) -> (X--1 : lt O n) -> lt (log p n) n
lt-log-n-n = λ (p : nat) -> λ (n : nat) -> λ (lt1p : lt (S O) p) -> λ (posn : lt O n) -> Or-ind lzero lzero lzero (lt (log p n) n) (eq lzero nat (log p n) n) (λ (X-x-170 : Or lzero lzero (lt (log p n) n) (eq lzero nat (log p n) n)) -> lt (log p n) n) (λ (X-x-171 : lt (log p n) n) -> X-x-171) (λ (Hn : eq lzero nat (log p n) n) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt (log p n) n) (absurd lzero (le (exp p n) n) (eq-ind lzero lzero nat (log p n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (log p n) x-1) -> le (exp p x-1) n) (le-exp-log p n posn) n Hn) (lt-to-not-le n (exp p n) (lt-m-exp-nm p n lt1p)))) (le-to-or-lt-eq (log p n) n (le-max-n (λ (x : nat) -> leb (exp p x) n) n))

lt-O-log : (p : nat) -> (n : nat) -> (X-- : lt (S O) n) -> (X--1 : le p n) -> lt O (log p n)
lt-O-log = λ (p : nat) -> λ (n : nat) -> λ (lt1p : lt (S O) n) -> λ (lepn : le p n) -> not-lt-to-le (max' n (λ (x : nat) -> leb (exp p x) n) O) (S O) (nmk lzero (lt (max' n (λ (x : nat) -> leb (exp p x) n) O) (S O)) (λ (H : lt (max' n (λ (x : nat) -> leb (exp p x) n) O) (S O)) -> eq-ind lzero lzero nat p (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat p x-1) -> (X-- : eq lzero bool (leb x-1 n) false) -> False lzero) (eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> (X--1 : eq lzero bool x false) -> False lzero) (λ (H0 : eq lzero bool true false) -> bool-discr lzero true false H0 (False lzero)) (leb p n) (le-to-leb-true p n lepn)) (exp p (S O)) (exp-n-1 p) (lt-max-to-false (λ (x : nat) -> leb (exp p x) n) n (S O) lt1p H)))

le-log-n-n : (p : nat) -> (n : nat) -> (X-- : lt (S O) p) -> le (log p n) n
le-log-n-n = λ (p : nat) -> λ (n : nat) -> λ (lt1p : lt (S O) p) -> match-nat lzero (λ (X-- : nat) -> le (log p X--) X--) (le-n (log p O)) (λ (m : nat) -> lt-to-le (log p (S m)) (S m) (lt-log-n-n p (S m) lt1p (lt-O-S m))) n

let-clause-1033 : (p : nat) -> (n : nat) -> (lt1p : lt (S O) p) -> (m : nat) -> (x2515 : nat) -> (x2516 : nat) -> eq lzero nat x2515 (plus (times x2516 (div x2515 x2516)) (mod x2515 x2516))
let-clause-1033 = λ (p : nat) -> λ (n : nat) -> λ (lt1p : lt (S O) p) -> λ (m : nat) -> λ (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)

lt-exp-log : (p : nat) -> (n : nat) -> (X-- : lt (S O) p) -> lt n (exp p (S (log p n)))
lt-exp-log = λ (p : nat) -> λ (n : nat) -> λ (lt1p : lt (S O) p) -> match-nat lzero (λ (X-- : nat) -> lt X-- (exp p (S (log p X--)))) (eq-ind lzero lzero nat p (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat p x-1) -> le (S O) x-1) (lt-to-le (S O) p lt1p) (plus p O) (plus-n-O p)) (λ (m : nat) -> not-le-to-lt (exp p (S (log p (S m)))) (S m) (leb-false-to-not-le (exp p (S (log p (S m)))) (S m) (lt-max-to-false (λ (X-- : nat) -> leb (exp p X--) (S m)) (S (S m)) (S (log p (S m))) (le-S-S (S (log p (S m))) (S m) (lt-log-n-n p (S m) lt1p (lt-O-S m))) (eq-ind lzero lzero nat (log p (S m)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (log p (S m)) x-1) -> lt x-1 (S (log p (S m)))) (eq-coerc lzero (lt (mod (log p (S m)) O) (plus (plus (mod (log p (S m)) O) (times O (div (log p (S m)) O))) (S O))) (lt (log p (S m)) (S (log p (S m)))) (lt-plus-Sn-r (mod (log p (S m)) O) (times O (div (log p (S m)) O)) O) (rewrite-l lzero (lsuc lzero) nat (log p (S m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (mod (log p (S m)) O) (plus X-- (S O))) (lt (log p (S m)) (S (log p (S m))))) (rewrite-l lzero (lsuc lzero) nat (log p (S m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (plus (log p (S m)) (S O))) (lt (log p (S m)) (S (log p (S m))))) (rewrite-l lzero (lsuc lzero) nat (S (log p (S m))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (log p (S m)) X--) (lt (log p (S m)) (S (log p (S m))))) (refl (lsuc lzero) (Set (lzero)) (lt (log p (S m)) (S (log p (S m))))) (plus (log p (S m)) (S O)) (rewrite-r lzero lzero nat (plus (log p (S m)) O) (λ (X-- : nat) -> eq lzero nat (S X--) (plus (log p (S m)) (S O))) (plus-n-Sm (log p (S m)) O) (log p (S m)) (plus-n-O (log p (S m))))) (mod (log p (S m)) O) (rewrite-r lzero lzero nat (plus O (mod (log p (S m)) O)) (λ (X-- : nat) -> eq lzero nat (log p (S m)) X--) (rewrite-l lzero lzero nat (plus (mod (log p (S m)) O) O) (λ (X-- : nat) -> eq lzero nat (log p (S m)) X--) (rewrite-r lzero lzero nat (times O (div (log p (S m)) O)) (λ (X-- : nat) -> eq lzero nat (log p (S m)) (plus (mod (log p (S m)) O) X--)) (rewrite-l lzero lzero nat (plus (times O (div (log p (S m)) O)) (mod (log p (S m)) O)) (λ (X-- : nat) -> eq lzero nat (log p (S m)) X--) (let-clause-1033 p n lt1p m (log p (S m)) O) (plus (mod (log p (S m)) O) (times O (div (log p (S m)) O))) (commutative-plus (times O (div (log p (S m)) O)) (mod (log p (S m)) O))) O (times-O-n (div (log p (S m)) O))) (plus O (mod (log p (S m)) O)) (commutative-plus (mod (log p (S m)) O) O)) (mod (log p (S m)) O) (plus-O-n (mod (log p (S m)) O)))) (plus (mod (log p (S m)) O) (times O (div (log p (S m)) O))) (rewrite-l lzero lzero nat (plus (times O (div (log p (S m)) O)) (mod (log p (S m)) O)) (λ (X-- : nat) -> eq lzero nat (log p (S m)) X--) (let-clause-1033 p n lt1p m (log p (S m)) O) (plus (mod (log p (S m)) O) (times O (div (log p (S m)) O))) (commutative-plus (times O (div (log p (S m)) O)) (mod (log p (S m)) O))))) (max'' (S (S m)) (λ (x : nat) -> leb (exp p x) (S m))) (tech-log p (S m) lt1p (lt-O-S m)))))) n

log-times1 : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : lt (S O) p) -> (X--1 : lt O n) -> (X--2 : lt O m) -> le (log p (times n m)) (S (plus (log p n) (log p m)))
log-times1 = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (lt1p : lt (S O) p) -> λ (posn : lt O n) -> λ (posm : lt O m) -> f-false-to-le-max (λ (x : nat) -> leb (exp p x) (times n m)) (times n m) (S (plus (log p n) (log p m))) (ex-intro lzero lzero nat (λ (i : nat) -> And lzero lzero (lt i (times n m)) (eq lzero bool (leb (exp p i) (times n m)) true)) O (conj lzero lzero (lt O (times n m)) (eq lzero bool (leb (exp p O) (times n m)) true) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> lt x (times n m)) (lt-times O n O m posn posm) O (times-n-O O)) (le-to-leb-true (exp p O) (times n m) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> le (S x) (times n m)) (lt-times O n O m posn posm) O (times-n-O O))))) (λ (i : nat) -> λ (Hm : lt (S (plus (log p n) (log p m))) i) -> lt-to-leb-false (exp p i) (times n m) (lt-to-le-to-lt (times n m) (times (exp p (S (log p n))) (exp p (S (log p m)))) (exp p i) (lt-times n (exp p (S (log p n))) m (exp p (S (log p m))) (lt-exp-log p n lt1p) (lt-exp-log p m lt1p)) (eq-ind lzero lzero nat (exp p (plus (S (log p n)) (S (log p m)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp p (plus (S (log p n)) (S (log p m)))) x-1) -> le x-1 (exp p i)) (le-exp (plus (S (log p n)) (S (log p m))) i p (lt-to-le (S O) p lt1p) (eq-ind lzero lzero nat (S (plus (max' n (λ (x : nat) -> leb (exp p x) n) O) (max' m (λ (x : nat) -> leb (exp p x) m) O))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (plus (max' n (λ (x : nat) -> leb (exp p x) n) O) (max' m (λ (x : nat) -> leb (exp p x) m) O))) x-1) -> le (S x-1) i) Hm (plus (max' n (λ (x : nat) -> leb (exp p x) n) O) (S (max' m (λ (x : nat) -> leb (exp p x) m) O))) (plus-n-Sm (max' n (λ (x : nat) -> leb (exp p x) n) O) (max' m (λ (x : nat) -> leb (exp p x) m) O)))) (times (exp p (S (log p n))) (exp p (S (log p m)))) (exp-plus-times p (S (log p n)) (S (log p m))))))

log-times : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : lt (S O) p) -> le (log p (times n m)) (S (plus (log p n) (log p m)))
log-times = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (lt1p : lt (S O) p) -> match-nat lzero (λ (X-- : nat) -> le (log p (times X-- m)) (S (plus (log p X--) (log p m)))) (eq-coerc lzero (le (minus (plus (log p O) (S (log p m))) (S (log p m))) (plus (log p O) (S (log p m)))) (le (log p (times O m)) (S (plus (log p O) (log p m)))) (minus-le (plus (log p O) (S (log p m))) (S (log p m))) (rewrite-l lzero (lsuc lzero) nat (log p O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus (log p O) (S (log p m)))) (le (log p (times O m)) (S (plus (log p O) (log p m))))) (rewrite-r lzero (lsuc lzero) nat (times m O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (log p O) (plus (log p O) (S (log p m)))) (le (log p X--) (S (plus (log p O) (log p m))))) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (log p O) (plus (log p O) (S (log p m)))) (le (log p X--) (S (plus (log p O) (log p m))))) (rewrite-r lzero (lsuc lzero) nat (plus (log p m) (log p O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (log p O) (plus (log p O) (S (log p m)))) (le (log p O) (S X--))) (rewrite-r lzero (lsuc lzero) nat (plus (log p m) (S (log p O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (log p O) (plus (log p O) (S (log p m)))) (le (log p O) X--)) (rewrite-r lzero (lsuc lzero) nat (plus (log p m) (S (log p O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (log p O) X--) (le (log p O) (plus (log p m) (S (log p O))))) (refl (lsuc lzero) (Set (lzero)) (le (log p O) (plus (log p m) (S (log p O))))) (plus (log p O) (S (log p m))) (rewrite-l lzero lzero nat (S (plus (log p O) (log p m))) (λ (X-- : nat) -> eq lzero nat X-- (plus (log p m) (S (log p O)))) (rewrite-l lzero lzero nat (plus (log p m) (log p O)) (λ (X-- : nat) -> eq lzero nat (S X--) (plus (log p m) (S (log p O)))) (plus-n-Sm (log p m) (log p O)) (plus (log p O) (log p m)) (commutative-plus (log p m) (log p O))) (plus (log p O) (S (log p m))) (plus-n-Sm (log p O) (log p m)))) (S (plus (log p m) (log p O))) (plus-n-Sm (log p m) (log p O))) (plus (log p O) (log p m)) (commutative-plus (log p O) (log p m))) (times m O) (times-n-O m)) (times O m) (commutative-times O m)) (minus (plus (log p O) (S (log p m))) (S (log p m))) (minus-plus-m-m (log p O) (S (log p m))))) (λ (n0 : nat) -> match-nat lzero (λ (X-- : nat) -> le (log p (times (S n0) X--)) (S (plus (log p (S n0)) (log p X--)))) (eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> le (log p x-1) (S (plus (log p (S n0)) (log p O)))) (le-O-n (S (plus (log p (S n0)) (log p O)))) (times (S n0) O) (times-n-O (S n0))) (λ (m0 : nat) -> log-times1 p (S n0) (S m0) lt1p (lt-O-S n0) (lt-O-S m0)) m) n

log-times-l : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : lt O n) -> (X--1 : lt O m) -> (X--2 : lt (S O) p) -> le (plus (log p n) (log p m)) (log p (times n m))
log-times-l = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (lt1p : lt (S O) p) -> true-to-le-max (λ (x : nat) -> leb (exp p x) (times n m)) (times n m) (plus (log p n) (log p m)) (match-le (S O) lzero (λ (X-- : nat) -> λ (X-0 : le (S O) X--) -> lt (plus (log p X--) (log p m)) (times X-- m)) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> lt (plus x (log p m)) (times (S O) m)) (eq-ind-r lzero lzero nat (times m (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times m (S O))) -> lt (plus O (log p m)) x) (eq-ind lzero lzero nat m (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat m x-1) -> lt (plus O (log p m)) x-1) (lt-log-n-n p m lt1p posm) (times m (S O)) (times-n-1 m)) (times (S O) m) (commutative-times (S O) m)) (log p (S O)) (log-SO p lt1p)) (λ (n0 : nat) -> λ (posn0 : le (S O) n0) -> match-le (S O) lzero (λ (X-- : nat) -> λ (X-0 : le (S O) X--) -> lt (plus (log p (S n0)) (log p X--)) (times (S n0) X--)) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> lt (plus (log p (S n0)) x) (times (S n0) (S O))) (eq-ind lzero lzero nat (log p (S n0)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (log p (S n0)) x-1) -> lt x-1 (times (S n0) (S O))) (eq-ind lzero lzero nat (S n0) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S n0) x-1) -> lt (log p (S n0)) x-1) (lt-log-n-n p (S n0) lt1p (lt-O-S n0)) (times (S n0) (S O)) (times-n-1 (S n0))) (plus (log p (S n0)) O) (plus-n-O (log p (S n0)))) (log p (S O)) (log-SO p lt1p)) (λ (m1 : nat) -> λ (lem1 : le (S O) m1) -> transitive-le (S (plus (log p (S n0)) (log p (S m1)))) (plus (S n0) (S m1)) (times (S n0) (S m1)) (le-S-S (plus (log p (S n0)) (log p (S m1))) (plus n0 (S m1)) (le-plus (log p (S n0)) n0 (log p (S m1)) (S m1) (le-S-S-to-le (log p (S n0)) n0 (lt-log-n-n p (S n0) lt1p (lt-O-S n0))) (le-max-n (λ (x : nat) -> leb (exp p x) (S m1)) (S m1)))) (le-S-S (plus n0 (S m1)) (plus m1 (times n0 (S m1))) (eq-ind-r lzero lzero nat (plus (S m1) n0) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S m1) n0)) -> le x (plus m1 (times n0 (S m1)))) (eq-ind-r lzero lzero nat (plus m1 (S n0)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus m1 (S n0))) -> le x (plus m1 (times n0 (S m1)))) (monotonic-le-plus-r m1 (S n0) (times n0 (S m1)) (eq-ind-r lzero lzero nat (times n0 (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times n0 (S O))) -> le (S x) (times n0 (S m1))) (monotonic-lt-times-r n0 posn0 (S O) (S m1) (le-S-S (S O) m1 lem1)) n0 (times-n-1 n0))) (S (plus m1 n0)) (plus-n-Sm m1 n0)) (plus n0 (S m1)) (commutative-plus n0 (S m1))))) m posm) n posn) (le-to-leb-true (exp p (plus (log p n) (log p m))) (times n m) (eq-ind-r lzero lzero nat (times (exp p (log p n)) (exp p (log p m))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p (log p n)) (exp p (log p m)))) -> le x (times n m)) (le-times (exp p (log p n)) n (exp p (log p m)) m (le-exp-log p n posn) (le-exp-log p m posm)) (exp p (plus (log p n) (log p m))) (exp-plus-times p (log p n) (log p m))))

log-exp : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : lt (S O) p) -> (X--1 : lt O m) -> eq lzero nat (log p (times (exp p n) m)) (plus n (log p m))
log-exp = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (lt1p : lt (S O) p) -> λ (posm : lt O m) -> max-spec-to-max (λ (x : nat) -> leb (exp p x) (times (exp p n) m)) (times (exp p n) m) (plus n (log p m)) (found-max-spec (times (exp p n) m) (λ (x : nat) -> leb (exp p x) (times (exp p n) m)) (plus n (log p m)) (nat-ind lzero (λ (X-x-365 : nat) -> lt (plus X-x-365 (log p m)) (times (exp p X-x-365) m)) (eq-ind lzero lzero nat (S O) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S O) x-1) -> lt (plus O (log p m)) (times x-1 m)) (eq-ind-r lzero lzero nat (times m (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times m (S O))) -> lt (plus O (log p m)) x) (eq-ind lzero lzero nat m (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat m x-1) -> lt (plus O (log p m)) x-1) (lt-log-n-n p m lt1p posm) (times m (S O)) (times-n-1 m)) (times (S O) m) (commutative-times (S O) m)) (exp p O) (exp-n-O p)) (λ (a : nat) -> λ (Hind : lt (plus a (log p m)) (times (exp p a) m)) -> lt-to-le-to-lt (S (plus a (log p m))) (S (times (exp p a) m)) (times (exp p (S a)) m) (le-S-S (S (plus a (log p m))) (times (exp p a) m) Hind) (eq-ind-r lzero lzero nat (times p (exp p a)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times p (exp p a))) -> le (S (times (exp p a) m)) (times x m)) (eq-ind-r lzero lzero nat (times p (times (exp p a) m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times p (times (exp p a) m))) -> le (S (times (exp p a) m)) x) (eq-ind-r lzero lzero nat (times (times (exp p a) m) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (times (exp p a) m) (S O))) -> le (S x) (times p (times (exp p a) m))) (eq-ind-r lzero lzero nat (times (S O) (times (exp p a) m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S O) (times (exp p a) m))) -> le (S x) (times p (times (exp p a) m))) (monotonic-lt-times-l (times (exp p a) m) (eq-ind-r lzero lzero nat (times O O) (λ (x : nat) -> λ (X-- : eq lzero nat x (times O O)) -> lt x (times (exp p a) m)) (lt-times O (exp p a) O m (lt-O-exp p a (lt-to-le (S O) p lt1p)) posm) O (times-n-O O)) (S O) p lt1p) (times (times (exp p a) m) (S O)) (commutative-times (times (exp p a) m) (S O))) (times (exp p a) m) (times-n-1 (times (exp p a) m))) (times (times p (exp p a)) m) (associative-times p (exp p a) m)) (times (exp p a) p) (commutative-times (exp p a) p))) n) (le-to-leb-true (exp p (plus n (log p m))) (times (exp p n) m) (eq-ind-r lzero lzero nat (times (exp p n) (exp p (log p m))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p n) (exp p (log p m)))) -> le x (times (exp p n) m)) (monotonic-le-times-r (exp p n) (exp p (log p m)) m (le-exp-log p m posm)) (exp p (plus n (log p m))) (exp-plus-times p n (log p m)))) (λ (i : nat) -> λ (Hi : lt (plus n (log p m)) i) -> λ (Hm : lt i (times (exp p n) m)) -> lt-to-leb-false (exp p i) (times (exp p n) m) (lt-to-le-to-lt (times (exp p n) m) (times (exp p n) (exp p (S (log p m)))) (exp p i) (monotonic-lt-times-r (exp p n) (lt-O-exp p n (lt-to-le (S O) p lt1p)) m (exp p (S (log p m))) (lt-exp-log p m lt1p)) (eq-ind lzero lzero nat (exp p (plus n (S (log p m)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp p (plus n (S (log p m)))) x-1) -> le x-1 (exp p i)) (le-exp (plus n (S (log p m))) i p (lt-to-le (S O) p lt1p) (eq-coerc lzero (le (S (plus n (log p m))) i) (le (plus n (S (log p m))) i) Hi (rewrite-r lzero (lsuc lzero) nat (plus n (S (log p m))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- i) (le (plus n (S (log p m))) i)) (refl (lsuc lzero) (Set (lzero)) (le (plus n (S (log p m))) i)) (S (plus n (log p m))) (plus-n-Sm n (log p m))))) (times (exp p n) (exp p (S (log p m)))) (exp-plus-times p n (S (log p m)))))))

eq-log-exp : (p : nat) -> (n : nat) -> (X-- : lt (S O) p) -> eq lzero nat (log p (exp p n)) n
eq-log-exp = λ (p : nat) -> λ (n : nat) -> λ (lt1p : lt (S O) p) -> eq-ind-r lzero lzero nat (times (exp p n) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p n) (S O))) -> eq lzero nat (log p x) n) (eq-ind-r lzero lzero nat (plus n (log p (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus n (log p (S O)))) -> eq lzero nat x n) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (plus n x) n) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat X-- n) (refl lzero nat n) (plus n O) (plus-n-O n)) (log p (S O)) (log-SO p lt1p)) (log p (times (exp p n) (S O))) (log-exp p n (S O) lt1p (lt-O-S O))) (exp p n) (times-n-1 (exp p n))

log-exp1 : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : lt (S O) p) -> le (log p (exp n m)) (times m (S (log p n)))
log-exp1 = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (lt1p : lt (S O) p) -> nat-ind lzero (λ (X-x-365 : nat) -> le (log p (exp n X-x-365)) (times X-x-365 (S (log p n)))) (le-x-times-x (log p (exp n O))) (λ (m0 : nat) -> λ (Hind : le (log p (exp n m0)) (times m0 (S (log p n)))) -> transitive-le (log p (exp n (S m0))) (S (plus (log p n) (log p (exp n m0)))) (times (S m0) (S (log p n))) (eq-ind-r lzero lzero nat (times n (exp n m0)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times n (exp n m0))) -> le (log p x) (S (plus (log p n) (log p (exp n m0))))) (log-times p n (exp n m0) lt1p) (times (exp n m0) n) (commutative-times (exp n m0) n)) (le-S-S (plus (log p n) (log p (exp n m0))) (plus (log p n) (times m0 (S (log p n)))) (monotonic-le-plus-r (log p n) (log p (exp n m0)) (times m0 (S (log p n))) Hind))) m

log-exp2 : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : lt (S O) p) -> (X--1 : lt O n) -> le (times m (log p n)) (log p (exp n m))
log-exp2 = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (ltp1 : lt (S O) p) -> λ (posn : lt O n) -> le-S-S-to-le (times m (log p n)) (log p (exp n m)) (lt-exp-to-lt p (times m (log p n)) (S (log p (exp n m))) (lt-to-le (S O) p ltp1) (eq-ind-r lzero lzero nat (times (log p n) m) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (log p n) m)) -> lt (exp p x) (exp p (S (log p (exp n m))))) (eq-ind lzero lzero nat (exp (exp p (log p n)) m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp (exp p (log p n)) m) x-1) -> lt x-1 (exp p (S (log p (exp n m))))) (le-to-lt-to-lt (exp (exp p (log p n)) m) (exp n m) (exp p (S (log p (exp n m)))) (nat-ind lzero (λ (X-x-365 : nat) -> le (exp (exp p (log p n)) X-x-365) (exp n X-x-365)) (le-n (exp (exp p (log p n)) O)) (λ (m0 : nat) -> λ (Hind : le (exp (exp p (log p n)) m0) (exp n m0)) -> le-times (exp (exp p (log p n)) m0) (exp n m0) (exp p (log p n)) n Hind (le-exp-log p n posn)) m) (lt-exp-log p (exp n m) ltp1)) (exp p (times (log p n) m)) (exp-exp-times p (log p n) m)) (times m (log p n)) (commutative-times m (log p n))))

le-log-S : (p : nat) -> (n : nat) -> (X-- : lt (S O) p) -> le (log p n) (log p (S n))
le-log-S = λ (p : nat) -> λ (n : nat) -> λ (lt1p : lt (S O) p) -> match-bool lzero (λ (X-- : bool) -> le (max' n (λ (x : nat) -> leb (exp p x) n) O) (match-bool lzero (λ (X-0 : bool) -> nat) n (max' n (λ (x : nat) -> leb (exp p x) (S n)) O) X--)) (le-max-n (λ (x : nat) -> leb (exp p x) n) n) (le-max-f-max-g (λ (x : nat) -> leb (exp p x) n) (λ (x : nat) -> leb (exp p x) (S n)) n (λ (i : nat) -> λ (ltin : lt i n) -> λ (H : eq lzero bool (leb (exp p i) n) true) -> le-to-leb-true (exp p i) (S n) (le-S (exp p i) n (leb-true-to-le (exp p i) n (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (leb (exp p i) n) H))))) (leb (exp p n) (S n))

le-log : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : lt (S O) p) -> (X--1 : le n m) -> le (log p n) (log p m)
le-log = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (lt1p : lt (S O) p) -> λ (lenm : le n m) -> le-ind lzero n (λ (x-417 : nat) -> λ (X-x-418 : le n x-417) -> le (log p n) (log p x-417)) (le-n (log p n)) (λ (m0 : nat) -> λ (lenm0 : le n m0) -> λ (Hind : le (log p n) (log p m0)) -> transitive-le (log p n) (log p m0) (log p (S m0)) Hind (le-log-S p m0 lt1p)) m lenm

log-div : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : lt (S O) p) -> (X--1 : lt O m) -> (X--2 : le m n) -> le (log p (div n m)) (minus (log p n) (log p m))
log-div = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (lt1p : lt (S O) p) -> λ (posn : lt O m) -> λ (lemn : le m n) -> le-plus-to-minus-r (log p (div n m)) (log p m) (log p n) (transitive-le (plus (log p (div n m)) (log p m)) (log p (times (div n m) m)) (log p n) (log-times-l p (div n m) m (le-times-to-le-div n m (S O) posn (eq-coerc lzero (le m n) (le (times m (S O)) n) lemn (rewrite-l lzero (lsuc lzero) nat (plus m (times m O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m n) (le X-- n)) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m n) (le (plus m X--) n)) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m n) (le X-- n)) (refl (lsuc lzero) (Set (lzero)) (le m n)) (plus m O) (plus-n-O m)) (times m O) (times-n-O m)) (times m (S O)) (times-n-Sm m O)))) posn lt1p) (le-log p (times (div n m) m) n lt1p (eq-coerc lzero (le (minus n (mod n m)) n) (le (times (div n m) m) n) (minus-le n (mod n m)) (rewrite-r lzero (lsuc lzero) nat (times m (div n m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus n (mod n m)) n) (le X-- n)) (rewrite-l lzero (lsuc lzero) nat (times m (div n m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- n) (le (times m (div n m)) n)) (refl (lsuc lzero) (Set (lzero)) (le (times m (div n m)) n)) (minus n (mod n m)) (rewrite-l lzero lzero nat (times (div n m) m) (λ (X-- : nat) -> eq lzero nat X-- (minus n (mod n m))) (eq-times-div-minus-mod n m) (times m (div n m)) (commutative-times (div n m) m))) (times (div n m) m) (commutative-times (div n m) m)))))

log-n-n : (n : nat) -> (X-- : lt (S O) n) -> eq lzero nat (log n n) (S O)
log-n-n = λ (n : nat) -> λ (lt1n : lt (S O) n) -> eq-ind-r lzero lzero nat (exp n (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (exp n (S O))) -> eq lzero nat (log n x) (S O)) (eq-ind-r lzero lzero nat (times (exp n (S O)) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp n (S O)) (S O))) -> eq lzero nat (log n x) (S O)) (eq-ind-r lzero lzero nat (plus (S O) (log n (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S O) (log n (S O)))) -> eq lzero nat x (S O)) (refl lzero nat (plus (S O) (log n (S O)))) (log n (times (exp n (S O)) (S O))) (log-exp n (S O) (S O) lt1n (lt-O-S O))) (exp n (S O)) (times-n-1 (exp n (S O)))) n (exp-n-1 n)

log-i-2n : (n : nat) -> (i : nat) -> (X-- : lt (S O) n) -> (X--1 : lt n i) -> (X--2 : le i (times (S (S O)) n)) -> eq lzero nat (log i (times (S (S O)) n)) (S O)
log-i-2n = λ (n : nat) -> λ (i : nat) -> λ (lt1n : lt (S O) n) -> λ (ltni : lt n i) -> λ (lei : le i (times (S (S O)) n)) -> match-Or lzero lzero (lt (log i (times (S (S O)) n)) (S O)) (eq lzero nat (log i (times (S (S O)) n)) (S O)) lzero (λ (X-- : Or lzero lzero (lt (log i (times (S (S O)) n)) (S O)) (eq lzero nat (log i (times (S (S O)) n)) (S O))) -> eq lzero nat (log i (times (S (S O)) n)) (S O)) (λ (ltab : lt (log i (times (S (S O)) n)) (S O)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat (log i (times (S (S O)) n)) (S O)) (absurd lzero (lt (log i (times (S (S O)) n)) (S O)) ltab (le-to-not-lt (S O) (log i (times (S (S O)) n)) (transitive-le (S O) (log i i) (log i (times (S (S O)) n)) (eq-ind lzero lzero nat (log i i) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (log i i) x-1) -> le x-1 (log i i)) (le-n (log i i)) (S O) (log-n-n i (transitive-lt (S O) n i lt1n ltni))) (le-log i i (times (S (S O)) n) (transitive-lt (S O) n i lt1n ltni) lei))))) (λ (auto : eq lzero nat (log i (times (S (S O)) n)) (S O)) -> rewrite-l lzero lzero nat (log i (times (S (S O)) n)) (λ (X-- : nat) -> eq lzero nat (log i (times (S (S O)) n)) X--) (refl lzero nat (log i (times (S (S O)) n))) (S O) auto) (le-to-or-lt-eq (log i (times (S (S O)) n)) (S O) (not-lt-to-le (S O) (log i (times (S (S O)) n)) (nmk lzero (lt (S O) (log i (times (S (S O)) n))) (λ (H : lt (S O) (log i (times (S (S O)) n))) -> absurd lzero (le (exp i (S (S O))) (times (S (S O)) n)) (transitive-le (exp i (S (S O))) (exp i (log i (times (S (S O)) n))) (times (S (S O)) n) (le-exp (S (S O)) (log i (times (S (S O)) n)) i (ltn-to-ltO n i ltni) H) (le-exp-log i (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 (S O) n lt1n)) O (times-n-O O)))) (lt-to-not-le (times (S (S O)) n) (exp i (S (S O))) (eq-ind-r lzero lzero nat (times i i) (λ (x : nat) -> λ (X-- : eq lzero nat x (times i i)) -> lt (times (S (S O)) n) x) (lt-times (S (S O)) i n i (le-to-lt-to-lt (S (S O)) n i lt1n ltni) (le-to-lt-to-lt n n i (le-n n) ltni)) (exp i (S (S O))) (exp-2 i)))))))

exp-n-O' : (n : nat) -> (X-- : lt O n) -> eq lzero nat (exp O n) O
exp-n-O' = λ (n : nat) -> λ (posn : lt O n) -> lt-O-n-elim lzero n posn (λ (X-- : nat) -> eq lzero nat (exp O X--) O) (λ (m : nat) -> rewrite-r lzero lzero nat (times O (exp O m)) (λ (X-- : nat) -> eq lzero nat X-- O) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat X-- O) (refl lzero nat O) (times O (exp O m)) (times-O-n (exp O m))) (times (exp O m) O) (commutative-times (exp O m) O))