-
Notifications
You must be signed in to change notification settings - Fork 0
/
matita-arithmetics-exp.agda
72 lines (48 loc) · 19 KB
/
matita-arithmetics-exp.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
open import Agda.Primitive
open import matita-basics-relations
open import matita-arithmetics-div-and-mod
open import matita-basics-logic
open import matita-arithmetics-nat
exp : (X---v : nat) -> (X--1-v : nat) -> nat
exp x O = (S O)
exp x (S y) = times (exp x y) x
exp-plus-times : (n : nat) -> (p : nat) -> (q : nat) -> eq lzero nat (exp n (plus p q)) (times (exp n p) (exp n q))
exp-plus-times = λ (n : nat) -> λ (p : nat) -> λ (q : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat (exp n (plus X-x-365 q)) (times (exp n X-x-365) (exp n q))) (rewrite-r lzero lzero nat (plus O (exp n q)) (λ (X-- : nat) -> eq lzero nat (exp n q) X--) (rewrite-l lzero lzero nat (exp n q) (λ (X-- : nat) -> eq lzero nat (exp n q) X--) (refl lzero nat (exp n q)) (plus O (exp n q)) (plus-O-n (exp n q))) (plus (exp n q) O) (commutative-plus (exp n q) O)) (λ (x-366 : nat) -> λ (X-x-368 : eq lzero nat (exp n (plus x-366 q)) (times (exp n x-366) (exp n q))) -> rewrite-r lzero lzero nat (plus q x-366) (λ (X-- : nat) -> eq lzero nat (times (exp n X--) n) (times (times (exp n x-366) n) (exp n q))) (rewrite-r lzero lzero nat (times (exp n q) (exp n x-366)) (λ (X-- : nat) -> eq lzero nat (times X-- n) (times (times (exp n x-366) n) (exp n q))) (rewrite-r lzero lzero nat (times n (times (exp n q) (exp n x-366))) (λ (X-- : nat) -> eq lzero nat X-- (times (times (exp n x-366) n) (exp n q))) (rewrite-r lzero lzero nat (times n (exp n x-366)) (λ (X-- : nat) -> eq lzero nat (times n (times (exp n q) (exp n x-366))) (times X-- (exp n q))) (rewrite-r lzero lzero nat (times (exp n q) (times n (exp n x-366))) (λ (X-- : nat) -> eq lzero nat (times n (times (exp n q) (exp n x-366))) X--) (rewrite-r lzero lzero nat (times n (times (exp n q) (exp n x-366))) (λ (X-- : nat) -> eq lzero nat (times n (times (exp n q) (exp n x-366))) X--) (refl lzero nat (times n (times (exp n q) (exp n x-366)))) (times (exp n q) (times n (exp n x-366))) (times-times (exp n q) n (exp n x-366))) (times (times n (exp n x-366)) (exp n q)) (commutative-times (times n (exp n x-366)) (exp n q))) (times (exp n x-366) n) (commutative-times (exp n x-366) n)) (times (times (exp n q) (exp n x-366)) n) (commutative-times (times (exp n q) (exp n x-366)) n)) (exp n (plus q x-366)) (rewrite-l lzero lzero nat (times (exp n x-366) (exp n q)) (λ (X-- : nat) -> eq lzero nat (exp n (plus q x-366)) X--) (rewrite-l lzero lzero nat (plus x-366 q) (λ (X-- : nat) -> eq lzero nat (exp n X--) (times (exp n x-366) (exp n q))) X-x-368 (plus q x-366) (commutative-plus x-366 q)) (times (exp n q) (exp n x-366)) (commutative-times (exp n x-366) (exp n q)))) (plus x-366 q) (commutative-plus x-366 q)) p
exp-n-O : (n : nat) -> eq lzero nat (S O) (exp n O)
exp-n-O = λ (n : nat) -> refl lzero nat (S O)
exp-n-1 : (n : nat) -> eq lzero nat n (exp n (S O))
exp-n-1 = λ (n : nat) -> rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) (plus n O) (plus-n-O n)
exp-1-n : (n : nat) -> eq lzero nat (S O) (exp (S O) n)
exp-1-n = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat (S O) (exp (S O) X-x-365)) (refl lzero nat (S O)) (λ (x-366 : nat) -> λ (X-x-368 : eq lzero nat (S O) (exp (S O) x-366)) -> rewrite-l lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (S O) (times X-- (S O))) (rewrite-l lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (S O) X--) (refl lzero nat (S O)) (times (S O) (S O)) (times-n-1 (S O))) (exp (S O) x-366) X-x-368) n
exp-2 : (n : nat) -> eq lzero nat (exp n (S (S O))) (times n n)
exp-2 = λ (n : nat) -> rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (times X-- n) (times n n)) (refl lzero nat (times n n)) (plus n O) (plus-n-O n)
exp-exp-times : (n : nat) -> (p : nat) -> (q : nat) -> eq lzero nat (exp (exp n p) q) (exp n (times p q))
exp-exp-times = λ (n : nat) -> λ (p : nat) -> λ (q : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat (exp (exp n p) X-x-365) (exp n (times p X-x-365))) (eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> eq lzero nat (S O) (exp n x-1)) (refl lzero nat (S O)) (times p O) (times-n-O p)) (λ (x-366 : nat) -> λ (X-x-368 : eq lzero nat (exp (exp n p) x-366) (exp n (times p x-366))) -> rewrite-r lzero lzero nat (times (exp n p) (exp (exp n p) x-366)) (λ (X-- : nat) -> eq lzero nat X-- (exp n (times p (S x-366)))) (rewrite-l lzero lzero nat (plus p (times p x-366)) (λ (X-- : nat) -> eq lzero nat (times (exp n p) (exp (exp n p) x-366)) (exp n X--)) (rewrite-r lzero lzero nat (times (exp n p) (exp n (times p x-366))) (λ (X-- : nat) -> eq lzero nat (times (exp n p) (exp (exp n p) x-366)) X--) (rewrite-l lzero lzero nat (exp (exp n p) x-366) (λ (X-- : nat) -> eq lzero nat (times (exp n p) (exp (exp n p) x-366)) (times (exp n p) X--)) (refl lzero nat (times (exp n p) (exp (exp n p) x-366))) (exp n (times p x-366)) X-x-368) (exp n (plus p (times p x-366))) (exp-plus-times n p (times p x-366))) (times p (S x-366)) (times-n-Sm p x-366)) (times (exp (exp n p) x-366) (exp n p)) (commutative-times (exp (exp n p) x-366) (exp n p))) q
lt-O-exp : (n : nat) -> (m : nat) -> (X-- : lt O n) -> lt O (exp n m)
lt-O-exp = λ (n : nat) -> λ (m : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (X-- : lt O n) -> lt O (exp n X-x-365)) (λ (auto : le (S O) n) -> lt-O-S O) (λ (a : nat) -> λ (Hind : (X-- : le (S O) n) -> le (S O) (exp n a)) -> λ (posn : le (S O) n) -> le-times (S O) (exp n a) (S O) n (Hind posn) posn) m
lt-m-exp-nm : (n : nat) -> (m : nat) -> (X-- : lt (S O) n) -> lt m (exp n m)
lt-m-exp-nm = λ (n : nat) -> λ (m : nat) -> λ (lt1n : lt (S O) n) -> nat-ind lzero (λ (X-x-365 : nat) -> lt X-x-365 (exp n X-x-365)) (lt-O-S O) (λ (n0 : nat) -> λ (Hind : le (S n0) (exp n n0)) -> transitive-le (S (S n0)) (times (S n0) (S (S O))) (times (exp n n0) n) (eq-coerc lzero (le (S (S n0)) (plus (plus (S n0) O) (S n0))) (le (S (S n0)) (times (S n0) (S (S O)))) (lt-plus-Sn-r (S n0) O n0) (rewrite-r lzero (lsuc lzero) nat (plus (S n0) (plus O (S n0))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (S n0)) X--) (le (S (S n0)) (times (S n0) (S (S O))))) (rewrite-l lzero (lsuc lzero) nat (plus (S n0) (times (S n0) (S O))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (S n0)) (plus (S n0) (plus O (S n0)))) (le (S (S n0)) X--)) (rewrite-l lzero (lsuc lzero) nat (plus (S n0) (times (S n0) O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (S n0)) (plus (S n0) (plus O (S n0)))) (le (S (S n0)) (plus (S n0) X--))) (rewrite-r lzero (lsuc lzero) nat (times O (S n0)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (S n0)) (plus (S n0) (plus O (S n0)))) (le (S (S n0)) (plus (S n0) (plus (S n0) X--)))) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (S n0)) (plus (S n0) (plus O (S n0)))) (le (S (S n0)) (plus (S n0) (plus (S n0) X--)))) (rewrite-r lzero (lsuc lzero) nat (plus O (S n0)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (S n0)) (plus (S n0) (plus O (S n0)))) (le (S (S n0)) (plus (S n0) X--))) (rewrite-l lzero (lsuc lzero) nat (S n0) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (S n0)) (plus (S n0) (plus O (S n0)))) (le (S (S n0)) (plus (S n0) X--))) (rewrite-l lzero (lsuc lzero) nat (S n0) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (S n0)) (plus (S n0) X--)) (le (S (S n0)) (plus (S n0) (S n0)))) (refl (lsuc lzero) (Set (lzero)) (le (S (S n0)) (plus (S n0) (S n0)))) (plus O (S n0)) (plus-O-n (S n0))) (plus O (S n0)) (plus-O-n (S n0))) (plus (S n0) O) (commutative-plus (S n0) O)) (times O (S n0)) (times-O-n (S n0))) (times (S n0) O) (commutative-times (S n0) O)) (times (S n0) (S O)) (times-n-Sm (S n0) O)) (times (S n0) (S (S O))) (times-n-Sm (S n0) (S O))) (plus (plus (S n0) O) (S n0)) (associative-plus (S n0) O (S n0)))) (le-times (S n0) (exp n n0) (S (S O)) n Hind lt1n)) m
exp-to-eq-O : (n : nat) -> (m : nat) -> (X-- : lt (S O) n) -> (X--1 : eq lzero nat (exp n m) (S O)) -> eq lzero nat m O
exp-to-eq-O = λ (n : nat) -> λ (m : nat) -> λ (ltin : lt (S O) n) -> λ (eq1 : eq lzero nat (exp n m) (S O)) -> le-to-le-to-eq m O (le-S-S-to-le m O (eq-ind lzero lzero nat (exp n m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (exp n m) x-1) -> le (S m) x-1) (lt-m-exp-nm n m ltin) (S O) eq1)) (le-O-n m)
let-clause-1258 : (b : nat) -> (lt1b : lt (S O) b) -> (n : nat) -> (H : eq lzero nat (times (exp b n) b) (S O)) -> eq lzero nat (times b (exp b n)) (S O)
let-clause-1258 = λ (b : nat) -> λ (lt1b : lt (S O) b) -> λ (n : nat) -> λ (H : eq lzero nat (times (exp b n) b) (S O)) -> rewrite-l lzero lzero nat (times (exp b n) b) (λ (X-- : nat) -> eq lzero nat X-- (S O)) H (times b (exp b n)) (commutative-times (exp b n) b)
injective-exp-r : (b : nat) -> (X-- : lt (S O) b) -> ||injective|| lzero lzero nat nat (λ (i : nat) -> exp b i)
injective-exp-r = λ (b : nat) -> λ (lt1b : lt (S O) b) -> nat-elim2 lzero (λ (X-- : nat) -> λ (X-0 : nat) -> (X--1 : eq lzero nat (exp b X--) (exp b X-0)) -> eq lzero nat X-- X-0) (λ (n : nat) -> λ (H : eq lzero nat (S O) (exp b n)) -> sym-eq lzero nat n O (exp-to-eq-O b n lt1b (rewrite-r lzero lzero nat (exp b n) (λ (X-- : nat) -> eq lzero nat (exp b n) X--) (refl lzero nat (exp b n)) (S O) H))) (λ (n : nat) -> λ (H : eq lzero nat (times (exp b n) b) (S O)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat (S n) O) (absurd lzero (lt (S O) (S O)) (eq-ind lzero lzero nat (times (exp b n) b) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (exp b n) b) x-1) -> lt (S O) x-1) (lt-to-le-to-lt (S O) (times (S O) b) (times (exp b n) b) (eq-coerc lzero (lt (S O) b) (lt (S O) (times (S O) b)) lt1b (rewrite-l lzero (lsuc lzero) nat (times b (exp b n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- b) (lt (S O) (times (S O) b))) (rewrite-l lzero (lsuc lzero) nat (times b (exp b n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (times b (exp b n)) b) (lt X-- (times (S O) b))) (rewrite-l lzero (lsuc lzero) nat (times b (exp b n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (times b (exp b n)) b) (lt (times b (exp b n)) (times X-- b))) (rewrite-r lzero (lsuc lzero) nat (times b (times b (exp b n))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (times b (exp b n)) b) (lt (times b (exp b n)) X--)) (rewrite-l lzero (lsuc lzero) nat b (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (times b (exp b n)) b) (lt (times b (exp b n)) X--)) (refl (lsuc lzero) (Set (lzero)) (lt (times b (exp b n)) b)) (times b (times b (exp b n))) (rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat b (times b X--)) (times-n-1 b) (times b (exp b n)) (let-clause-1258 b lt1b n H))) (times (times b (exp b n)) b) (commutative-times (times b (exp b n)) b)) (S O) (let-clause-1258 b lt1b n H)) (S O) (let-clause-1258 b lt1b n H)) (S O) (let-clause-1258 b lt1b n H))) (le-times (S O) (exp b n) b b (lt-O-exp b n (lt-S-to-lt O b lt1b)) (le-n b))) (S O) H) (not-le-Sn-n (S O)))) (λ (n : nat) -> λ (m : nat) -> λ (Hind : (X-- : eq lzero nat (exp b n) (exp b m)) -> eq lzero nat n m) -> λ (H : eq lzero nat (times (exp b n) b) (times (exp b m) b)) -> eq-f lzero lzero nat nat S n m (Hind (injective-times-l b (lt-S-to-lt O b lt1b) (exp b n) (exp b m) H)))
le-exp : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : lt O p) -> (X--1 : le n m) -> le (exp p n) (exp p m)
le-exp = nat-elim2 lzero (λ (X-- : nat) -> λ (X-0 : nat) -> (p : nat) -> (X--1 : lt O p) -> (X--2 : le X-- X-0) -> le (exp p X--) (exp p X-0)) (λ (n : nat) -> λ (m : nat) -> λ (ltm : lt O m) -> λ (len : le O n) -> lt-O-exp m n ltm) (λ (n : nat) -> λ (m : nat) -> λ (X-- : lt O m) -> λ (len : le (S n) O) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> le (exp m (S n)) (exp m O)) (absurd lzero (le (S n) O) len (not-le-Sn-O n))) (λ (n : nat) -> λ (m : nat) -> λ (Hind : (p : nat) -> (X-- : lt O p) -> (X--1 : le n m) -> le (exp p n) (exp p m)) -> λ (p : nat) -> λ (posp : lt O p) -> λ (lenm : le (S n) (S m)) -> le-times (exp p n) (exp p m) p p (Hind p posp (eq-coerc lzero (le (pred (S n)) (pred (S m))) (le n m) (monotonic-pred (S n) (S m) lenm) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (pred (S m))) (le n m)) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n X--) (le n m)) (refl (lsuc lzero) (Set (lzero)) (le n m)) (pred (S m)) (pred-Sn m)) (pred (S n)) (pred-Sn n)))) (le-n p))
le-exp1 : (n : nat) -> (m : nat) -> (a : nat) -> (X-- : lt O a) -> (X--1 : le n m) -> le (exp n a) (exp m a)
le-exp1 = λ (n : nat) -> λ (m : nat) -> λ (a : nat) -> λ (posa : lt O a) -> λ (lenm : le n m) -> le-ind lzero (S O) (λ (x-417 : nat) -> λ (X-x-418 : le (S O) x-417) -> le (exp n x-417) (exp m x-417)) (eq-coerc lzero (le n m) (le (exp n (S O)) (exp m (S O))) lenm (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n m) (le X-- (exp m (S O)))) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n m) (le n X--)) (refl (lsuc lzero) (Set (lzero)) (le n m)) (exp m (S O)) (exp-n-1 m)) (exp n (S O)) (exp-n-1 n))) (λ (a0 : nat) -> λ (posa0 : le (S O) a0) -> λ (Hind : le (exp n a0) (exp m a0)) -> le-times (exp n a0) (exp m a0) n m Hind lenm) a posa
lt-exp : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : lt (S O) p) -> (X--1 : lt n m) -> lt (exp p n) (exp p m)
lt-exp = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (lt1p : lt (S O) p) -> λ (ltnm : lt n m) -> match-Or lzero lzero (lt (exp p n) (exp p m)) (eq lzero nat (exp p n) (exp p m)) lzero (λ (X-- : Or lzero lzero (lt (exp p n) (exp p m)) (eq lzero nat (exp p n) (exp p m))) -> lt (exp p n) (exp p m)) (λ (auto : lt (exp p n) (exp p m)) -> auto) (λ (eqexp : eq lzero nat (exp p n) (exp p m)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt (exp p n) (exp p m)) (absurd lzero (eq lzero nat n m) (injective-exp-r p lt1p n m (rewrite-r lzero lzero nat (exp p m) (λ (X-- : nat) -> eq lzero nat X-- (exp p m)) (refl lzero nat (exp p m)) (exp p n) eqexp)) (lt-to-not-eq n m ltnm))) (le-to-or-lt-eq (exp p n) (exp p m) (le-exp n m p (lt-S-to-lt O p lt1p) (lt-to-le n m ltnm)))
lt-exp1 : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : lt O p) -> (X--1 : lt n m) -> lt (exp n p) (exp m p)
lt-exp1 = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (posp : lt O p) -> λ (ltnm : lt n m) -> le-ind lzero (S O) (λ (x-417 : nat) -> λ (X-x-418 : le (S O) x-417) -> lt (exp n x-417) (exp m x-417)) (eq-coerc lzero (lt n m) (lt (exp n (S O)) (exp m (S O))) ltnm (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt n m) (lt X-- (exp m (S O)))) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt n m) (lt n X--)) (refl (lsuc lzero) (Set (lzero)) (lt n m)) (exp m (S O)) (exp-n-1 m)) (exp n (S O)) (exp-n-1 n))) (λ (p0 : nat) -> λ (posp0 : le (S O) p0) -> λ (Hind : lt (exp n p0) (exp m p0)) -> lt-times (exp n p0) (exp m p0) n m Hind ltnm) p posp
le-exp-to-le : (b : nat) -> (n : nat) -> (m : nat) -> (X-- : lt (S O) b) -> (X--1 : le (exp b n) (exp b m)) -> le n m
le-exp-to-le = λ (b : nat) -> λ (n : nat) -> λ (m : nat) -> λ (lt1b : lt (S O) b) -> λ (leexp : le (exp b n) (exp b m)) -> match-Or lzero lzero (le n m) (Not lzero (le n m)) lzero (λ (X-- : Or lzero lzero (le n m) (Not lzero (le n m))) -> le n m) (λ (auto : le n m) -> auto) (λ (notle : Not lzero (le n m)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> le n m) (absurd lzero (le (exp b n) (exp b m)) leexp (lt-to-not-le (exp b m) (exp b n) (lt-exp m n b lt1b (not-le-to-lt n m notle))))) (decidable-le n m)
le-exp-to-le1 : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : lt O p) -> (X--1 : le (exp n p) (exp m p)) -> le n m
le-exp-to-le1 = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (posp : lt O p) -> λ (leexp : le (exp n p) (exp m p)) -> not-lt-to-le m n (not-to-not lzero (lt m n) (lt (exp m p) (exp n p)) (lt-exp1 m n p posp) (le-to-not-lt (exp n p) (exp m p) leexp))
lt-exp-to-lt : (a : nat) -> (n : nat) -> (m : nat) -> (X-- : lt O a) -> (X--1 : lt (exp a n) (exp a m)) -> lt n m
lt-exp-to-lt = λ (a : nat) -> λ (n : nat) -> λ (m : nat) -> λ (lt1a : lt O a) -> λ (ltexp : lt (exp a n) (exp a m)) -> match-Or lzero lzero (le (S n) m) (Not lzero (le (S n) m)) lzero (λ (X-- : Or lzero lzero (le (S n) m) (Not lzero (le (S n) m))) -> lt n m) (λ (auto : le (S n) m) -> auto) (λ (H : Not lzero (le (S n) m)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt n m) (absurd lzero (lt (exp a n) (exp a m)) ltexp (le-to-not-lt (exp a m) (exp a n) (le-exp m n a lt1a (not-lt-to-le n m H))))) (decidable-le (S n) m)
lt-exp-to-lt1 : (a : nat) -> (n : nat) -> (m : nat) -> (X-- : lt O a) -> (X--1 : lt (exp n a) (exp m a)) -> lt n m
lt-exp-to-lt1 = λ (a : nat) -> λ (n : nat) -> λ (m : nat) -> λ (posa : lt O a) -> λ (ltexp : lt (exp n a) (exp m a)) -> match-Or lzero lzero (le (S n) m) (Not lzero (le (S n) m)) lzero (λ (X-- : Or lzero lzero (le (S n) m) (Not lzero (le (S n) m))) -> lt n m) (λ (auto : le (S n) m) -> auto) (λ (H : Not lzero (le (S n) m)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt n m) (absurd lzero (lt (exp n a) (exp m a)) ltexp (le-to-not-lt (exp m a) (exp n a) (le-exp1 m n a posa (not-lt-to-le n m H))))) (decidable-le (S n) m)
times-exp : (n : nat) -> (m : nat) -> (p : nat) -> eq lzero nat (times (exp n p) (exp m p)) (exp (times n m) p)
times-exp = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat (times (exp n X-x-365) (exp m X-x-365)) (exp (times n m) X-x-365)) (refl lzero nat (times (exp n O) (exp m O))) (λ (p0 : nat) -> λ (Hind : eq lzero nat (times (exp n p0) (exp m p0)) (exp (times n m) p0)) -> rewrite-r lzero lzero nat (times n (exp n p0)) (λ (X-- : nat) -> eq lzero nat (times X-- (times (exp m p0) m)) (times (exp (times n m) p0) (times n m))) (rewrite-r lzero lzero nat (times m (exp m p0)) (λ (X-- : nat) -> eq lzero nat (times (times n (exp n p0)) X--) (times (exp (times n m) p0) (times n m))) (rewrite-r lzero lzero nat (times n (times (exp n p0) (times m (exp m p0)))) (λ (X-- : nat) -> eq lzero nat X-- (times (exp (times n m) p0) (times n m))) (rewrite-r lzero lzero nat (times m (times (exp n p0) (exp m p0))) (λ (X-- : nat) -> eq lzero nat (times n X--) (times (exp (times n m) p0) (times n m))) (rewrite-r lzero lzero nat (exp (times n m) p0) (λ (X-- : nat) -> eq lzero nat (times n (times m X--)) (times (exp (times n m) p0) (times n m))) (rewrite-r lzero lzero nat (times (times n m) (exp (times n m) p0)) (λ (X-- : nat) -> eq lzero nat (times n (times m (exp (times n m) p0))) X--) (rewrite-r lzero lzero nat (times n (times m (exp (times n m) p0))) (λ (X-- : nat) -> eq lzero nat (times n (times m (exp (times n m) p0))) X--) (refl lzero nat (times n (times m (exp (times n m) p0)))) (times (times n m) (exp (times n m) p0)) (associative-times n m (exp (times n m) p0))) (times (exp (times n m) p0) (times n m)) (commutative-times (exp (times n m) p0) (times n m))) (times (exp n p0) (exp m p0)) Hind) (times (exp n p0) (times m (exp m p0))) (times-times (exp n p0) m (exp m p0))) (times (times n (exp n p0)) (times m (exp m p0))) (associative-times n (exp n p0) (times m (exp m p0)))) (times (exp m p0) m) (commutative-times (exp m p0) m)) (times (exp n p0) n) (commutative-times (exp n p0) n)) p