-
Notifications
You must be signed in to change notification settings - Fork 0
/
matita-arithmetics-ord.agda
145 lines (97 loc) · 93.1 KB
/
matita-arithmetics-ord.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
open import Agda.Primitive
open import matita-arithmetics-gcd
open import matita-arithmetics-exp
open import matita-arithmetics-primes
open import matita-basics-types
open import matita-basics-logic
open import matita-arithmetics-div-and-mod
open import matita-arithmetics-nat
p-ord-aux : (X---v : nat) -> (X--1-v : nat) -> (X--2-v : nat) -> Prod lzero lzero nat nat
p-ord-aux O n m = match-nat lzero (λ (X--1-v : nat) -> Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (a-v : nat) -> mk-Prod lzero lzero nat nat O n) (mod n m)
p-ord-aux (S p) n m = match-nat lzero (λ (X--1-v : nat) -> Prod lzero lzero nat nat) ( match-Prod lzero lzero nat nat lzero (λ (X--1-v : Prod lzero lzero nat nat) -> Prod lzero lzero nat nat) (λ (q-v : nat) -> λ (r-v : nat) -> mk-Prod lzero lzero nat nat (S q-v) r-v) (p-ord-aux p (div n m) m)) (λ (a-v : nat) -> mk-Prod lzero lzero nat nat O n) (mod n m)
p-ord : (X-n : nat) -> (X-m : nat) -> Prod lzero lzero nat nat
p-ord = λ (n : nat) -> λ (m : nat) -> p-ord-aux n n m
p-ord-aux-0 : (n : nat) -> (m : nat) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux O n m) (mk-Prod lzero lzero nat nat O n)
p-ord-aux-0 = λ (n : nat) -> λ (m : nat) -> match-nat lzero (λ (X-- : nat) -> eq lzero (Prod lzero lzero nat nat) (match-nat lzero (λ (X-0 : nat) -> Prod lzero lzero nat nat) (match-nat lzero (λ (X-0 : nat) -> Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (p0 : nat) -> match-Prod lzero lzero nat nat lzero (λ (X-0 : Prod lzero lzero nat nat) -> Prod lzero lzero nat nat) (λ (q : nat) -> λ (r : nat) -> mk-Prod lzero lzero nat nat (S q) r) (p-ord-aux p0 (div n m) m)) O) (λ (a : nat) -> mk-Prod lzero lzero nat nat O n) X--) (mk-Prod lzero lzero nat nat O n)) (refl lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n)) (λ (auto : nat) -> refl lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n)) (mod n m)
p-ord-aux-Strue : (n : nat) -> (m : nat) -> (p : nat) -> (q : nat) -> (r : nat) -> (X-- : eq lzero nat (mod n m) O) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p (div n m) m) (mk-Prod lzero lzero nat nat q r)) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S p) n m) (mk-Prod lzero lzero nat nat (S q) r)
p-ord-aux-Strue = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (q : nat) -> λ (r : nat) -> λ (H : eq lzero nat (mod n m) O) -> eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p (div n m) m) (mk-Prod lzero lzero nat nat q r)) -> eq lzero (Prod lzero lzero nat nat) (match-nat lzero (λ (X-0 : nat) -> Prod lzero lzero nat nat) (match-nat lzero (λ (X-0 : nat) -> Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (p0 : nat) -> match-Prod lzero lzero nat nat lzero (λ (X-0 : Prod lzero lzero nat nat) -> Prod lzero lzero nat nat) (λ (q0 : nat) -> λ (r0 : nat) -> mk-Prod lzero lzero nat nat (S q0) r0) (p-ord-aux p0 (div n m) m)) (S p)) (λ (a : nat) -> mk-Prod lzero lzero nat nat O n) x) (mk-Prod lzero lzero nat nat (S q) r)) (λ (Hord : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p (div n m) m) (mk-Prod lzero lzero nat nat q r)) -> eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat q r) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat q r)) -> eq lzero (Prod lzero lzero nat nat) (match-Prod lzero lzero nat nat lzero (λ (X-0 : Prod lzero lzero nat nat) -> Prod lzero lzero nat nat) (λ (q0 : nat) -> λ (r0 : nat) -> mk-Prod lzero lzero nat nat (S q0) r0) x) (mk-Prod lzero lzero nat nat (S q) r)) (refl lzero (Prod lzero lzero nat nat) (match-Prod lzero lzero nat nat lzero (λ (X-0 : Prod lzero lzero nat nat) -> Prod lzero lzero nat nat) (λ (q0 : nat) -> λ (r0 : nat) -> mk-Prod lzero lzero nat nat (S q0) r0) (mk-Prod lzero lzero nat nat q r))) (p-ord-aux p (div n m) m) Hord) (mod n m) H
p-ord-aux-false : (p : nat) -> (n : nat) -> (m : nat) -> (a : nat) -> (X-- : eq lzero nat (mod n m) (S a)) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux p n m) (mk-Prod lzero lzero nat nat O n)
p-ord-aux-false = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (a : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : eq lzero nat (mod n m) (S a)) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux X-- n m) (mk-Prod lzero lzero nat nat O n)) (λ (H : eq lzero nat (mod n m) (S a)) -> eq-ind-r lzero lzero nat (S a) (λ (x : nat) -> λ (X-- : eq lzero nat x (S a)) -> eq lzero (Prod lzero lzero nat nat) (match-nat lzero (λ (X-0 : nat) -> Prod lzero lzero nat nat) (match-nat lzero (λ (X-0 : nat) -> Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (p0 : nat) -> match-Prod lzero lzero nat nat lzero (λ (X-0 : Prod lzero lzero nat nat) -> Prod lzero lzero nat nat) (λ (q : nat) -> λ (r : nat) -> mk-Prod lzero lzero nat nat (S q) r) (p-ord-aux p0 (div n m) m)) O) (λ (a0 : nat) -> mk-Prod lzero lzero nat nat O n) x) (mk-Prod lzero lzero nat nat O n)) (refl lzero (Prod lzero lzero nat nat) (match-nat lzero (λ (X-0 : nat) -> Prod lzero lzero nat nat) (match-nat lzero (λ (X-0 : nat) -> Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (p0 : nat) -> match-Prod lzero lzero nat nat lzero (λ (X-0 : Prod lzero lzero nat nat) -> Prod lzero lzero nat nat) (λ (q : nat) -> λ (r : nat) -> mk-Prod lzero lzero nat nat (S q) r) (p-ord-aux p0 (div n m) m)) O) (λ (a0 : nat) -> mk-Prod lzero lzero nat nat O n) (S a))) (mod n m) H) (λ (p1 : nat) -> λ (H : eq lzero nat (mod n m) (S a)) -> eq-ind-r lzero lzero nat (S a) (λ (x : nat) -> λ (X-- : eq lzero nat x (S a)) -> eq lzero (Prod lzero lzero nat nat) (match-nat lzero (λ (X-0 : nat) -> Prod lzero lzero nat nat) (match-nat lzero (λ (X-0 : nat) -> Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (p0 : nat) -> match-Prod lzero lzero nat nat lzero (λ (X-0 : Prod lzero lzero nat nat) -> Prod lzero lzero nat nat) (λ (q : nat) -> λ (r : nat) -> mk-Prod lzero lzero nat nat (S q) r) (p-ord-aux p0 (div n m) m)) (S p1)) (λ (a0 : nat) -> mk-Prod lzero lzero nat nat O n) x) (mk-Prod lzero lzero nat nat O n)) (refl lzero (Prod lzero lzero nat nat) (match-nat lzero (λ (X-- : nat) -> Prod lzero lzero nat nat) (match-nat lzero (λ (X-- : nat) -> Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (p0 : nat) -> match-Prod lzero lzero nat nat lzero (λ (X-- : Prod lzero lzero nat nat) -> Prod lzero lzero nat nat) (λ (q : nat) -> λ (r : nat) -> mk-Prod lzero lzero nat nat (S q) r) (p-ord-aux p0 (div n m) m)) (S p1)) (λ (a0 : nat) -> mk-Prod lzero lzero nat nat O n) (S a))) (mod n m) H) p
p-ord-degenerate : (p : nat) -> (n : nat) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux p n (S O)) (mk-Prod lzero lzero nat nat p n)
p-ord-degenerate = λ (p : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (n : nat) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux X-x-365 n (S O)) (mk-Prod lzero lzero nat nat X-x-365 n)) (λ (n : nat) -> rewrite-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (X-- : Prod lzero lzero nat nat) -> eq lzero (Prod lzero lzero nat nat) X-- (mk-Prod lzero lzero nat nat O n)) (refl lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n)) (p-ord-aux O n (S O)) (p-ord-aux-0 n (S O))) (λ (p1 : nat) -> λ (Hind : (n : nat) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 n (S O)) (mk-Prod lzero lzero nat nat p1 n)) -> λ (n : nat) -> eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S p1) (div n (S O))) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat (S p1) (div n (S O)))) -> eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat (S p1) n)) (eq-ind-r lzero lzero nat (plus (times (div n (S O)) (S O)) (mod n (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (div n (S O)) (S O)) (mod n (S O)))) -> eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S p1) (div n (S O))) (mk-Prod lzero lzero nat nat (S p1) x)) (rewrite-r lzero lzero nat (times (S O) (div n (S O))) (λ (X-- : nat) -> eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S p1) (div n (S O))) (mk-Prod lzero lzero nat nat (S p1) (plus X-- (mod n (S O))))) (rewrite-r lzero lzero nat O (λ (X-- : nat) -> eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S p1) (div n (S O))) (mk-Prod lzero lzero nat nat (S p1) (plus (times (S O) (div n (S O))) X--))) (rewrite-r lzero lzero nat (plus O (times (S O) (div n (S O)))) (λ (X-- : nat) -> eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S p1) (div n (S O))) (mk-Prod lzero lzero nat nat (S p1) X--)) (rewrite-l lzero lzero nat (times (S O) (div n (S O))) (λ (X-- : nat) -> eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S p1) (div n (S O))) (mk-Prod lzero lzero nat nat (S p1) X--)) (rewrite-l lzero lzero nat (times (S O) (div n (S O))) (λ (X-- : nat) -> eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S p1) X--) (mk-Prod lzero lzero nat nat (S p1) (times (S O) (div n (S O))))) (refl lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S p1) (times (S O) (div n (S O))))) (div n (S O)) (rewrite-r lzero lzero nat (times (div n (S O)) (S O)) (λ (X-- : nat) -> eq lzero nat (times (S O) (div n (S O))) X--) (commutative-times (S O) (div n (S O))) (div n (S O)) (times-n-1 (div n (S O))))) (plus O (times (S O) (div n (S O)))) (plus-O-n (times (S O) (div n (S O))))) (plus (times (S O) (div n (S O))) O) (commutative-plus (times (S O) (div n (S O))) O)) (mod n (S O)) (divides-to-mod-O (S O) n (lt-O-S O) (divides-SO-n n))) (times (div n (S O)) (S O)) (commutative-times (div n (S O)) (S O))) n (div-mod n (S O))) (p-ord-aux (S p1) n (S O)) (p-ord-aux-Strue n (S O) p1 p1 (div n (S O)) (rewrite-r lzero lzero nat O (λ (X-- : nat) -> eq lzero nat X-- O) (refl lzero nat O) (mod n (S O)) (divides-to-mod-O (S O) n (lt-O-S O) (divides-SO-n n))) (Hind (div n (S O))))) p
p-ord-aux-to-exp : (p : nat) -> (n : nat) -> (m : nat) -> (q : nat) -> (r : nat) -> (X-- : lt O m) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p n m) (mk-Prod lzero lzero nat nat q r)) -> eq lzero nat n (times (exp m q) r)
p-ord-aux-to-exp = λ (p : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (n : nat) -> (m : nat) -> (q : nat) -> (r : nat) -> (X-- : lt O m) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux X-x-365 n m) (mk-Prod lzero lzero nat nat q r)) -> eq lzero nat n (times (exp m q) r)) (λ (n : nat) -> λ (m : nat) -> nat-case lzero (mod n m) (λ (X-- : nat) -> (q : nat) -> (r : nat) -> (X--1 : lt O m) -> (X--2 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux O n m) (mk-Prod lzero lzero nat nat q r)) -> eq lzero nat n (times (exp m q) r)) (λ (Hmod : eq lzero nat (mod n m) O) -> λ (q : nat) -> λ (r : nat) -> λ (posm : lt O m) -> eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat O n)) -> (X--1 : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat q r)) -> eq lzero nat n (times (exp m q) r)) (λ (Hqr : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat q r)) -> Prod-discr lzero lzero lzero nat nat (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat q r) Hqr (eq lzero nat n (times (exp m q) r)) (λ (e0 : eq lzero nat (R0 lzero nat O) q) -> eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat x-1 r)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) n x-1 X-x-2) r) -> eq lzero nat n (times (exp m x-1) r)) (λ (Hqr0 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat O r)) -> λ (e00 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) n O (refl lzero nat O)) r) -> eq-ind-r lzero lzero nat r (λ (x : nat) -> λ (X-- : eq lzero nat x r) -> (X--1 : eq lzero nat (mod x m) O) -> (X--2 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O x) (mk-Prod lzero lzero nat nat O r)) -> eq lzero nat x (times (exp m O) r)) (λ (Hmod0 : eq lzero nat (mod r m) O) -> λ (Hqr1 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (mk-Prod lzero lzero nat nat O r)) -> streicherK lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (λ (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (mk-Prod lzero lzero nat nat O r)) -> eq lzero nat r (times (exp m O) r)) (rewrite-r lzero lzero nat (times (exp m O) r) (λ (X-- : nat) -> eq lzero nat X-- (times (exp m O) r)) (refl lzero nat (times (exp m O) r)) r (rewrite-r lzero lzero nat (plus r O) (λ (X-- : nat) -> eq lzero nat X-- (times (exp m O) r)) (rewrite-r lzero lzero nat (times O r) (λ (X-- : nat) -> eq lzero nat (plus r X--) (times (exp m O) r)) (rewrite-l lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (plus r (times O r)) (times X-- r)) (times-Sn-m O r) (exp m O) (exp-n-O m)) O (times-O-n r)) r (plus-n-O r))) Hqr1) n e00 Hmod Hqr0) q e0 Hqr)) (p-ord-aux O n m) (p-ord-aux-0 n m)) (λ (a : nat) -> λ (H : eq lzero nat (mod n m) (S a)) -> λ (q : nat) -> λ (r : nat) -> λ (posm : lt O m) -> eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat O n)) -> (X--1 : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat q r)) -> eq lzero nat n (times (exp m q) r)) (λ (Hqr : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat q r)) -> Prod-discr lzero lzero lzero nat nat (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat q r) Hqr (eq lzero nat n (times (exp m q) r)) (λ (e0 : eq lzero nat (R0 lzero nat O) q) -> eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat x-1 r)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) n x-1 X-x-2) r) -> eq lzero nat n (times (exp m x-1) r)) (λ (Hqr0 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat O r)) -> λ (e00 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) n O (refl lzero nat O)) r) -> eq-ind-r lzero lzero nat r (λ (x : nat) -> λ (X-- : eq lzero nat x r) -> (X--1 : eq lzero nat (mod x m) (S a)) -> (X--2 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O x) (mk-Prod lzero lzero nat nat O r)) -> eq lzero nat x (times (exp m O) r)) (λ (H0 : eq lzero nat (mod r m) (S a)) -> λ (Hqr1 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (mk-Prod lzero lzero nat nat O r)) -> streicherK lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (λ (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (mk-Prod lzero lzero nat nat O r)) -> eq lzero nat r (times (exp m O) r)) (rewrite-r lzero lzero nat (times (exp m O) r) (λ (X-- : nat) -> eq lzero nat X-- (times (exp m O) r)) (refl lzero nat (times (exp m O) r)) r (rewrite-r lzero lzero nat (plus r O) (λ (X-- : nat) -> eq lzero nat X-- (times (exp m O) r)) (rewrite-r lzero lzero nat (times O r) (λ (X-- : nat) -> eq lzero nat (plus r X--) (times (exp m O) r)) (rewrite-l lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (plus r (times O r)) (times X-- r)) (times-Sn-m O r) (exp m O) (exp-n-O m)) O (times-O-n r)) r (plus-n-O r))) Hqr1) n e00 H Hqr0) q e0 Hqr)) (p-ord-aux O n m) (p-ord-aux-false O n m a H))) (λ (p1 : nat) -> λ (Hind : (n : nat) -> (m : nat) -> (q : nat) -> (r : nat) -> (X-- : lt O m) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 n m) (mk-Prod lzero lzero nat nat q r)) -> eq lzero nat n (times (exp m q) r)) -> λ (n : nat) -> λ (m : nat) -> nat-case lzero (mod n m) (λ (X-- : nat) -> (q : nat) -> (r : nat) -> (X--1 : lt O m) -> (X--2 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S p1) n m) (mk-Prod lzero lzero nat nat q r)) -> eq lzero nat n (times (exp m q) r)) (λ (Hmod : eq lzero nat (mod n m) O) -> λ (q : nat) -> λ (r : nat) -> λ (posm : lt O m) -> match-Prod lzero lzero nat nat lzero (λ (X-- : Prod lzero lzero nat nat) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (div n m) m) X--) -> (X--2 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S p1) n m) (mk-Prod lzero lzero nat nat q r)) -> eq lzero nat n (times (exp m q) r)) (λ (q1 : nat) -> λ (r1 : nat) -> λ (H1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (div n m) m) (mk-Prod lzero lzero nat nat q1 r1)) -> eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r1) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat (S q1) r1)) -> (X--1 : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat q r)) -> eq lzero nat n (times (exp m q) r)) (λ (H : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r1) (mk-Prod lzero lzero nat nat q r)) -> Prod-discr lzero lzero lzero nat nat (mk-Prod lzero lzero nat nat (S q1) r1) (mk-Prod lzero lzero nat nat q r) H (eq lzero nat n (times (exp m q) r)) (λ (e0 : eq lzero nat (R0 lzero nat (S q1)) q) -> eq-ind lzero lzero nat (S q1) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S q1) x-1) -> (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r1) (mk-Prod lzero lzero nat nat x-1 r)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat (S q1) (λ (x0 : nat) -> λ (p0 : eq lzero nat (S q1) x0) -> nat) r1 x-1 X-x-2) r) -> eq lzero nat n (times (exp m x-1) r)) (λ (H0 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r1) (mk-Prod lzero lzero nat nat (S q1) r)) -> λ (e00 : eq lzero nat (R1 lzero lzero nat (S q1) (λ (x0 : nat) -> λ (p0 : eq lzero nat (S q1) x0) -> nat) r1 (S q1) (refl lzero nat (S q1))) r) -> eq-ind-r lzero lzero nat r (λ (x : nat) -> λ (X-- : eq lzero nat x r) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (div n m) m) (mk-Prod lzero lzero nat nat q1 x)) -> (X--2 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) x) (mk-Prod lzero lzero nat nat (S q1) r)) -> eq lzero nat n (times (exp m (S q1)) r)) (λ (H10 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (div n m) m) (mk-Prod lzero lzero nat nat q1 r)) -> λ (H2 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r) (mk-Prod lzero lzero nat nat (S q1) r)) -> streicherK lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r) (λ (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r) (mk-Prod lzero lzero nat nat (S q1) r)) -> eq lzero nat n (times (exp m (S q1)) r)) (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))) -> eq lzero nat x (times (times (exp m q1) m) r)) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (plus (times (div n m) m) x) (times (times (exp m q1) m) r)) (eq-ind lzero lzero nat (times (div n m) m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (div n m) m) x-1) -> eq lzero nat x-1 (times (times (exp m q1) m) r)) (eq-ind-r lzero lzero nat (times (exp m q1) r) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp m q1) r)) -> eq lzero nat (times x m) (times (times (exp m q1) m) r)) (rewrite-r lzero lzero nat (times r (exp m q1)) (λ (X-- : nat) -> eq lzero nat (times X-- m) (times (times (exp m q1) m) r)) (rewrite-r lzero lzero nat (times m (times r (exp m q1))) (λ (X-- : nat) -> eq lzero nat X-- (times (times (exp m q1) m) r)) (rewrite-r lzero lzero nat (times m (exp m q1)) (λ (X-- : nat) -> eq lzero nat (times m (times r (exp m q1))) (times X-- r)) (rewrite-r lzero lzero nat (times r (times m (exp m q1))) (λ (X-- : nat) -> eq lzero nat (times m (times r (exp m q1))) X--) (rewrite-r lzero lzero nat (times m (times r (exp m q1))) (λ (X-- : nat) -> eq lzero nat (times m (times r (exp m q1))) X--) (refl lzero nat (times m (times r (exp m q1)))) (times r (times m (exp m q1))) (times-times r m (exp m q1))) (times (times m (exp m q1)) r) (commutative-times (times m (exp m q1)) r)) (times (exp m q1) m) (commutative-times (exp m q1) m)) (times (times r (exp m q1)) m) (commutative-times (times r (exp m q1)) m)) (times (exp m q1) r) (commutative-times (exp m q1) r)) (div n m) (Hind (div n m) m q1 r posm H10)) (plus (times (div n m) m) O) (plus-n-O (times (div n m) m))) (mod n m) Hmod) n (div-mod n m)) H2) r1 e00 H1 H0) q e0 H)) (p-ord-aux (S p1) n m) (p-ord-aux-Strue n m p1 q1 r1 Hmod H1)) (p-ord-aux p1 (div n m) m) (refl lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (div n m) m))) (λ (a : nat) -> λ (H : eq lzero nat (mod n m) (S a)) -> λ (q : nat) -> λ (r : nat) -> λ (posm : lt O m) -> eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat O n)) -> (X--1 : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat q r)) -> eq lzero nat n (times (exp m q) r)) (λ (Hqr : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat q r)) -> Prod-discr lzero lzero lzero nat nat (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat q r) Hqr (eq lzero nat n (times (exp m q) r)) (λ (e0 : eq lzero nat (R0 lzero nat O) q) -> eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat x-1 r)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) n x-1 X-x-2) r) -> eq lzero nat n (times (exp m x-1) r)) (λ (Hqr0 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat O r)) -> λ (e00 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) n O (refl lzero nat O)) r) -> eq-ind-r lzero lzero nat r (λ (x : nat) -> λ (X-- : eq lzero nat x r) -> (X--1 : eq lzero nat (mod x m) (S a)) -> (X--2 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O x) (mk-Prod lzero lzero nat nat O r)) -> eq lzero nat x (times (exp m O) r)) (λ (H0 : eq lzero nat (mod r m) (S a)) -> λ (Hqr1 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (mk-Prod lzero lzero nat nat O r)) -> streicherK lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (λ (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (mk-Prod lzero lzero nat nat O r)) -> eq lzero nat r (times (exp m O) r)) (rewrite-r lzero lzero nat (times (exp m O) r) (λ (X-- : nat) -> eq lzero nat X-- (times (exp m O) r)) (refl lzero nat (times (exp m O) r)) r (rewrite-r lzero lzero nat (plus r O) (λ (X-- : nat) -> eq lzero nat X-- (times (exp m O) r)) (rewrite-r lzero lzero nat (times O r) (λ (X-- : nat) -> eq lzero nat (plus r X--) (times (exp m O) r)) (rewrite-l lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (plus r (times O r)) (times X-- r)) (times-Sn-m O r) (exp m O) (exp-n-O m)) O (times-O-n r)) r (plus-n-O r))) Hqr1) n e00 H Hqr0) q e0 Hqr)) (p-ord-aux (S p1) n m) (p-ord-aux-false (S p1) n m a H))) p
p-ord-exp : (n : nat) -> (m : nat) -> (i : nat) -> (X-- : lt O m) -> (X--1 : Not lzero (eq lzero nat (mod n m) O)) -> (p : nat) -> (X--2 : le i p) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux p (times (exp m i) n) m) (mk-Prod lzero lzero nat nat i n)
p-ord-exp = λ (n : nat) -> λ (m : nat) -> λ (i : nat) -> λ (posm : lt O m) -> λ (Hmod : Not lzero (eq lzero nat (mod n m) O)) -> match-ex lzero lzero nat (λ (a : nat) -> eq lzero nat (mod n m) (S a)) lzero (λ (X-- : ex lzero lzero nat (λ (a : nat) -> eq lzero nat (mod n m) (S a))) -> (p : nat) -> (X--1 : le i p) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux p (times (exp m i) n) m) (mk-Prod lzero lzero nat nat i n)) (λ (mod1 : nat) -> λ (Hmod1 : eq lzero nat (mod n m) (S mod1)) -> nat-ind lzero (λ (X-x-365 : nat) -> (p : nat) -> (X-- : le X-x-365 p) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux p (times (exp m X-x-365) n) m) (mk-Prod lzero lzero nat nat X-x-365 n)) (λ (p : nat) -> λ (posp : le O p) -> eq-ind lzero lzero nat n (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat n x-1) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux p x-1 m) (mk-Prod lzero lzero nat nat O n)) (p-ord-aux-false p n m mod1 Hmod1) (plus n O) (plus-n-O n)) (λ (i0 : nat) -> λ (Hind : (p : nat) -> (X-- : le i0 p) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux p (times (exp m i0) n) m) (mk-Prod lzero lzero nat nat i0 n)) -> λ (p : nat) -> nat-case lzero p (λ (X-- : nat) -> (X--1 : le (S i0) X--) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux X-- (times (exp m (S i0)) n) m) (mk-Prod lzero lzero nat nat (S i0) n)) (λ (Hp : eq lzero nat p O) -> eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> (X--1 : le (S i0) O) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux O (times (exp m (S i0)) n) m) (mk-Prod lzero lzero nat nat (S i0) n)) (λ (Habs : le (S i0) O) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux O (times (exp m (S i0)) n) m) (mk-Prod lzero lzero nat nat (S i0) n)) (absurd lzero (le (S i0) O) Habs (not-le-Sn-O i0))) p Hp) (λ (p1 : nat) -> λ (Hp1 : eq lzero nat p (S p1)) -> λ (lep1 : le (S i0) (S p1)) -> p-ord-aux-Strue (times (exp m (S i0)) n) m p1 i0 n (divides-to-mod-O m (times (times (exp m i0) m) n) posm (quotient m (times (times (exp m i0) m) n) (times (exp m i0) n) (rewrite-r lzero lzero nat (times m (exp m i0)) (λ (X-- : nat) -> eq lzero nat (times X-- n) (times m (times (exp m i0) n))) (rewrite-r lzero lzero nat (times n (times m (exp m i0))) (λ (X-- : nat) -> eq lzero nat X-- (times m (times (exp m i0) n))) (rewrite-r lzero lzero nat (times n (exp m i0)) (λ (X-- : nat) -> eq lzero nat (times n (times m (exp m i0))) (times m X--)) (rewrite-r lzero lzero nat (times n (times m (exp m i0))) (λ (X-- : nat) -> eq lzero nat (times n (times m (exp m i0))) X--) (refl lzero nat (times n (times m (exp m i0)))) (times m (times n (exp m i0))) (times-times m n (exp m i0))) (times (exp m i0) n) (commutative-times (exp m i0) n)) (times (times m (exp m i0)) n) (commutative-times (times m (exp m i0)) n)) (times (exp m i0) m) (commutative-times (exp m i0) m)))) (eq-ind lzero lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (times (exp m i0) n) m) (λ (x-1 : Prod lzero lzero nat nat) -> λ (X-x-2 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (times (exp m i0) n) m) x-1) -> eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (div (times (exp m (S i0)) n) m) m) x-1) (eq-f2 lzero lzero lzero nat nat (Prod lzero lzero nat nat) (p-ord-aux p1) (div (times (exp m (S i0)) n) m) (times (exp m i0) n) m m (eq-ind-r lzero lzero nat (times (exp m i0) (times m n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp m i0) (times m n))) -> eq lzero nat (div x m) (times (exp m i0) n)) (eq-ind-r lzero lzero nat (times n m) (λ (x : nat) -> λ (X-- : eq lzero nat x (times n m)) -> eq lzero nat (div (times (exp m i0) x) m) (times (exp m i0) n)) (eq-ind lzero lzero nat (times (times (exp m i0) n) m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (exp m i0) n) m) x-1) -> eq lzero nat (div x-1 m) (times (exp m i0) n)) (eq-ind-r lzero lzero nat (times (exp m i0) n) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp m i0) n)) -> eq lzero nat x (times (exp m i0) n)) (rewrite-r lzero lzero nat (times n (exp m i0)) (λ (X-- : nat) -> eq lzero nat X-- (times (exp m i0) n)) (rewrite-r lzero lzero nat (times n (exp m i0)) (λ (X-- : nat) -> eq lzero nat (times n (exp m i0)) X--) (refl lzero nat (times n (exp m i0))) (times (exp m i0) n) (commutative-times (exp m i0) n)) (times (exp m i0) n) (commutative-times (exp m i0) n)) (div (times (times (exp m i0) n) m) m) (div-times (times (exp m i0) n) m posm)) (times (exp m i0) (times n m)) (associative-times (exp m i0) n m)) (times m n) (commutative-times m n)) (times (times (exp m i0) m) n) (associative-times (exp m i0) m n)) (refl lzero nat m)) (mk-Prod lzero lzero nat nat i0 n) (Hind p1 (le-S-S-to-le i0 p1 lep1))))) i) (nat-case lzero (mod n m) (λ (X-- : nat) -> ex lzero lzero nat (λ (a : nat) -> eq lzero nat X-- (S a))) (λ (H : eq lzero nat (mod n m) O) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> ex lzero lzero nat (λ (a : nat) -> eq lzero nat O (S a))) (absurd lzero (eq lzero nat (mod n m) O) (rewrite-r lzero lzero nat O (λ (X-- : nat) -> eq lzero nat X-- O) (refl lzero nat O) (mod n m) H) Hmod)) (λ (a : nat) -> λ (Hmod1 : eq lzero nat (mod n m) (S a)) -> ex-intro lzero lzero nat (λ (a0 : nat) -> eq lzero nat (S a) (S a0)) a (rewrite-l lzero lzero nat (mod n m) (λ (X-- : nat) -> eq lzero nat X-- (S a)) (rewrite-l lzero lzero nat (mod n m) (λ (X-- : nat) -> eq lzero nat (mod n m) X--) (refl lzero nat (mod n m)) (S a) Hmod1) (S a) Hmod1)))
p-ord-aux-to-not-mod-O : (p : nat) -> (n : nat) -> (m : nat) -> (q : nat) -> (r : nat) -> (X-- : lt (S O) m) -> (X--1 : lt O n) -> (X--2 : le n p) -> (X--3 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p n m) (mk-Prod lzero lzero nat nat q r)) -> Not lzero (eq lzero nat (mod r m) O)
p-ord-aux-to-not-mod-O = λ (p : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (n : nat) -> (m : nat) -> (q : nat) -> (r : nat) -> (X-- : lt (S O) m) -> (X--1 : lt O n) -> (X--2 : le n X-x-365) -> (X--3 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux X-x-365 n m) (mk-Prod lzero lzero nat nat q r)) -> Not lzero (eq lzero nat (mod r m) O)) (λ (n : nat) -> λ (m : nat) -> λ (q : nat) -> λ (r : nat) -> λ (X-- : lt (S O) m) -> λ (posn : lt O n) -> λ (nposn : le n O) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux O n m) (mk-Prod lzero lzero nat nat q r)) -> Not lzero (eq lzero nat (mod r m) O)) (absurd lzero (lt O n) posn (le-to-not-lt n O nposn))) (λ (p1 : nat) -> λ (Hind : (n : nat) -> (m : nat) -> (q : nat) -> (r : nat) -> (X-- : lt (S O) m) -> (X--1 : lt O n) -> (X--2 : le n p1) -> (X--3 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 n m) (mk-Prod lzero lzero nat nat q r)) -> Not lzero (eq lzero nat (mod r m) O)) -> λ (n : nat) -> λ (m : nat) -> nat-case lzero (mod n m) (λ (X-- : nat) -> (q : nat) -> (r : nat) -> (X--1 : lt (S O) m) -> (X--2 : lt O n) -> (X--3 : le n (S p1)) -> (X--4 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S p1) n m) (mk-Prod lzero lzero nat nat q r)) -> Not lzero (eq lzero nat (mod r m) O)) (λ (Hmod : eq lzero nat (mod n m) O) -> λ (q : nat) -> λ (r : nat) -> λ (lt1m : lt (S O) m) -> λ (posn : lt O n) -> λ (len : le n (S p1)) -> match-Prod lzero lzero nat nat lzero (λ (X-- : Prod lzero lzero nat nat) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (div n m) m) X--) -> (X--2 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S p1) n m) (mk-Prod lzero lzero nat nat q r)) -> Not lzero (eq lzero nat (mod r m) O)) (λ (q1 : nat) -> λ (r1 : nat) -> λ (H1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (div n m) m) (mk-Prod lzero lzero nat nat q1 r1)) -> eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r1) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat (S q1) r1)) -> (X--1 : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat q r)) -> Not lzero (eq lzero nat (mod r m) O)) (λ (H : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r1) (mk-Prod lzero lzero nat nat q r)) -> Prod-discr lzero lzero lzero nat nat (mk-Prod lzero lzero nat nat (S q1) r1) (mk-Prod lzero lzero nat nat q r) H (Not lzero (eq lzero nat (mod r m) O)) (λ (e0 : eq lzero nat (R0 lzero nat (S q1)) q) -> eq-ind lzero lzero nat (S q1) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S q1) x-1) -> (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r1) (mk-Prod lzero lzero nat nat x-1 r)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat (S q1) (λ (x0 : nat) -> λ (p0 : eq lzero nat (S q1) x0) -> nat) r1 x-1 X-x-2) r) -> Not lzero (eq lzero nat (mod r m) O)) (λ (H0 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r1) (mk-Prod lzero lzero nat nat (S q1) r)) -> λ (e00 : eq lzero nat (R1 lzero lzero nat (S q1) (λ (x0 : nat) -> λ (p0 : eq lzero nat (S q1) x0) -> nat) r1 (S q1) (refl lzero nat (S q1))) r) -> eq-ind-r lzero lzero nat r (λ (x : nat) -> λ (X-- : eq lzero nat x r) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (div n m) m) (mk-Prod lzero lzero nat nat q1 x)) -> (X--2 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) x) (mk-Prod lzero lzero nat nat (S q1) r)) -> Not lzero (eq lzero nat (mod r m) O)) (λ (H10 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (div n m) m) (mk-Prod lzero lzero nat nat q1 r)) -> λ (H2 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r) (mk-Prod lzero lzero nat nat (S q1) r)) -> streicherK lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r) (λ (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S q1) r) (mk-Prod lzero lzero nat nat (S q1) r)) -> Not lzero (eq lzero nat (mod r m) O)) (Hind (div n m) m q1 r lt1m (pos-div n m (lt-to-le (S O) m lt1m) posn Hmod) (le-S-S-to-le (div n m) p1 (transitive-le (S (div n m)) n (S p1) (lt-times-to-lt-div n n m (eq-ind-r lzero lzero nat (times n (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times n (S O))) -> lt x (times n m)) (monotonic-lt-times-r n posn (S O) m lt1m) n (times-n-1 n))) len)) H10) H2) r1 e00 H1 H0) q e0 H)) (p-ord-aux (S p1) n m) (p-ord-aux-Strue n m p1 q1 r1 Hmod H1)) (p-ord-aux p1 (div n m) m) (refl lzero (Prod lzero lzero nat nat) (p-ord-aux p1 (div n m) m))) (λ (a : nat) -> λ (H : eq lzero nat (mod n m) (S a)) -> λ (q : nat) -> λ (r : nat) -> λ (lt1m : lt (S O) m) -> λ (posn : lt O n) -> λ (posm : le n (S p1)) -> eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat O n)) -> (X--1 : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat q r)) -> Not lzero (eq lzero nat (mod r m) O)) (λ (Hqr : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat q r)) -> Prod-discr lzero lzero lzero nat nat (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat q r) Hqr (Not lzero (eq lzero nat (mod r m) O)) (λ (e0 : eq lzero nat (R0 lzero nat O) q) -> eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat x-1 r)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) n x-1 X-x-2) r) -> Not lzero (eq lzero nat (mod r m) O)) (λ (Hqr0 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O n) (mk-Prod lzero lzero nat nat O r)) -> λ (e00 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) n O (refl lzero nat O)) r) -> eq-ind-r lzero lzero nat r (λ (x : nat) -> λ (X-- : eq lzero nat x r) -> (X--1 : eq lzero nat (mod x m) (S a)) -> (X--2 : lt O x) -> (X--3 : le x (S p1)) -> (X--4 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O x) (mk-Prod lzero lzero nat nat O r)) -> Not lzero (eq lzero nat (mod r m) O)) (λ (H0 : eq lzero nat (mod r m) (S a)) -> λ (posn0 : lt O r) -> λ (posm0 : le r (S p1)) -> λ (Hqr1 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (mk-Prod lzero lzero nat nat O r)) -> streicherK lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (λ (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O r) (mk-Prod lzero lzero nat nat O r)) -> Not lzero (eq lzero nat (mod r m) O)) (eq-ind-r lzero lzero nat (S a) (λ (x : nat) -> λ (X-- : eq lzero nat x (S a)) -> Not lzero (eq lzero nat x O)) (sym-not-eq lzero nat O (S a) (not-eq-O-S a)) (mod r m) H0) Hqr1) n e00 H posn posm Hqr0) q e0 Hqr)) (p-ord-aux (S p1) n m) (p-ord-aux-false (S p1) n m a H))) p
let-clause-1033''''' : (p : nat) -> (n : nat) -> (q : nat) -> (r : nat) -> (posp : lt O p) -> (ndivpr : Not lzero (divides p r)) -> (Hn : eq lzero nat n (times (exp p q) r)) -> (q0 : nat) -> (q1 : nat) -> (Hind : le (S q1) (exp p (S q1))) -> (x2515 : nat) -> (x2516 : nat) -> eq lzero nat x2515 (plus (times x2516 (div x2515 x2516)) (mod x2515 x2516))
let-clause-1033''''' = λ (p : nat) -> λ (n : nat) -> λ (q : nat) -> λ (r : nat) -> λ (posp : lt O p) -> λ (ndivpr : Not lzero (divides p r)) -> λ (Hn : eq lzero nat n (times (exp p q) r)) -> λ (q0 : nat) -> λ (q1 : nat) -> λ (Hind : le (S q1) (exp p (S q1))) -> λ (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)
p-ord-exp1 : (p : nat) -> (n : nat) -> (q : nat) -> (r : nat) -> (X-- : lt O p) -> (X--1 : Not lzero (divides p r)) -> (X--2 : eq lzero nat n (times (exp p q) r)) -> eq lzero (Prod lzero lzero nat nat) (p-ord n p) (mk-Prod lzero lzero nat nat q r)
p-ord-exp1 = λ (p : nat) -> λ (n : nat) -> λ (q : nat) -> λ (r : nat) -> λ (posp : lt O p) -> λ (ndivpr : Not lzero (divides p r)) -> λ (Hn : eq lzero nat n (times (exp p q) r)) -> eq-ind-r lzero lzero nat (times (exp p q) r) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p q) r)) -> eq lzero (Prod lzero lzero nat nat) (p-ord x p) (mk-Prod lzero lzero nat nat q r)) (p-ord-exp r p q posp (not-to-not lzero (eq lzero nat (mod r p) O) (divides p r) (λ (auto : eq lzero nat (mod r p) O) -> eq-coerc lzero (divides p (minus r O)) (divides p r) (eq-mod-to-divides r O p posp (rewrite-r lzero lzero nat O (λ (X-- : nat) -> eq lzero nat X-- (mod O p)) (rewrite-r lzero lzero nat O (λ (X-- : nat) -> eq lzero nat O X--) (refl lzero nat O) (mod O p) (mod-O-n p)) (mod r p) auto)) (rewrite-l lzero (lsuc lzero) nat r (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (divides p X--) (divides p r)) (refl (lsuc lzero) (Set (lzero)) (divides p r)) (minus r O) (minus-n-O r))) ndivpr) (times (exp p q) r) (transitive-le q (exp p q) (times (exp p q) r) (nat-ind lzero (λ (X-x-365 : nat) -> le X-x-365 (exp p X-x-365)) (le-O-n (exp p O)) (λ (q0 : nat) -> match-nat lzero (λ (X-- : nat) -> (X-x-368 : le X-- (exp p X--)) -> le (S X--) (exp p (S X--))) (λ (X-- : le O (exp p O)) -> 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 (match-Or lzero lzero (lt (S O) p) (eq lzero nat (S O) p) lzero (λ (X-0 : Or lzero lzero (lt (S O) p) (eq lzero nat (S O) p)) -> lt (S O) p) (λ (auto : lt (S O) p) -> auto) (λ (eqp1 : eq lzero nat (S O) p) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt (S O) p) (absurd lzero (divides p r) (eq-ind lzero lzero nat (S O) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S O) x-1) -> divides x-1 r) (quotient (S O) r r (rewrite-r lzero lzero nat p (λ (X--1 : nat) -> eq lzero nat r (times X--1 r)) (rewrite-r lzero lzero nat (times r p) (λ (X--1 : nat) -> eq lzero nat r X--1) (rewrite-l lzero lzero nat r (λ (X--1 : nat) -> eq lzero nat r X--1) (refl lzero nat r) (times r p) (rewrite-l lzero lzero nat (S O) (λ (X--1 : nat) -> eq lzero nat r (times r X--1)) (times-n-1 r) p eqp1)) (times p r) (commutative-times p r)) (S O) eqp1)) p eqp1) ndivpr)) (le-to-or-lt-eq (S O) p posp))) (plus p O) (plus-n-O p)) (λ (q1 : nat) -> λ (Hind : le (S q1) (exp p (S q1))) -> lt-to-le-to-lt (S q1) (times (S q1) (S (S O))) (exp p (S (S q1))) (eq-ind-r lzero lzero nat (times (S q1) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S q1) (S O))) -> lt x (times (S q1) (S (S O)))) (monotonic-lt-times-r (S q1) (lt-O-S q1) (S O) (S (S O)) (eq-coerc lzero (lt (mod (S O) O) (plus (plus (mod (S O) O) (times O (div (S O) O))) (S O))) (lt (S O) (S (S O))) (lt-plus-Sn-r (mod (S O) O) (times O (div (S O) O)) O) (rewrite-l lzero (lsuc lzero) nat (S O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (mod (S O) O) (plus X-- (S O))) (lt (S O) (S (S O)))) (rewrite-l lzero (lsuc lzero) nat (S O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (plus (S O) (S O))) (lt (S O) (S (S O)))) (rewrite-r lzero (lsuc lzero) nat (S (S O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (S O) X--) (lt (S O) (S (S O)))) (refl (lsuc lzero) (Set (lzero)) (lt (S O) (S (S O)))) (plus (S O) (S O)) (rewrite-r lzero lzero nat (times (S O) (S O)) (λ (X-- : nat) -> eq lzero nat (plus (S O) X--) (S (S O))) (rewrite-r lzero lzero nat (times (S (S O)) (S O)) (λ (X-- : nat) -> eq lzero nat (plus (S O) (times (S O) (S O))) X--) (times-Sn-m (S O) (S O)) (S (S O)) (times-n-1 (S (S O)))) (S O) (times-n-1 (S O)))) (mod (S O) O) (rewrite-r lzero lzero nat (plus O (mod (S O) O)) (λ (X-- : nat) -> eq lzero nat (S O) X--) (rewrite-l lzero lzero nat (plus (mod (S O) O) O) (λ (X-- : nat) -> eq lzero nat (S O) X--) (rewrite-r lzero lzero nat (times O (div (S O) O)) (λ (X-- : nat) -> eq lzero nat (S O) (plus (mod (S O) O) X--)) (rewrite-l lzero lzero nat (plus (times O (div (S O) O)) (mod (S O) O)) (λ (X-- : nat) -> eq lzero nat (S O) X--) (let-clause-1033''''' p n q r posp ndivpr Hn q0 q1 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-1033''''' p n q r posp ndivpr Hn q0 q1 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)))))) (S q1) (times-n-1 (S q1))) (le-times (S q1) (exp p (S q1)) (S (S O)) p Hind (match-Or lzero lzero (lt (S O) p) (eq lzero nat (S O) p) lzero (λ (X-- : Or lzero lzero (lt (S O) p) (eq lzero nat (S O) p)) -> lt (S O) p) (λ (auto : lt (S O) p) -> auto) (λ (eqp1 : eq lzero nat (S O) p) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt (S O) p) (absurd lzero (divides p r) (eq-ind lzero lzero nat (S O) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S O) x-1) -> divides x-1 r) (quotient (S O) r r (rewrite-r lzero lzero nat p (λ (X-- : nat) -> eq lzero nat r (times X-- r)) (rewrite-r lzero lzero nat (times r p) (λ (X-- : nat) -> eq lzero nat r X--) (rewrite-l lzero lzero nat r (λ (X-- : nat) -> eq lzero nat r X--) (refl lzero nat r) (times r p) (rewrite-l lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat r (times r X--)) (times-n-1 r) p eqp1)) (times p r) (commutative-times p r)) (S O) eqp1)) p eqp1) ndivpr)) (le-to-or-lt-eq (S O) p posp)))) q0) q) (eq-ind-r lzero lzero nat (times (exp p q) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p q) (S O))) -> le x (times (exp p q) r)) (le-times (exp p q) (exp p q) (S O) r (le-n (exp p q)) (match-nat lzero (λ (X-- : nat) -> (X--1 : Not lzero (divides p X--)) -> le (S O) X--) (λ (Habs : Not lzero (divides p O)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> le (S O) O) (absurd lzero (divides p O) (quotient p O O (rewrite-r lzero lzero nat (times p O) (λ (X-- : nat) -> eq lzero nat X-- (times p O)) (refl lzero nat (times p O)) O (times-n-O p))) Habs)) (λ (auto : nat) -> λ (auto' : Not lzero (divides p (S auto))) -> lt-O-S auto) r ndivpr)) (exp p q) (times-n-1 (exp p q))))) n Hn
p-ord-to-exp1 : (p : nat) -> (n : nat) -> (q : nat) -> (r : nat) -> (X-- : lt (S O) p) -> (X--1 : lt O n) -> (X--2 : eq lzero (Prod lzero lzero nat nat) (p-ord n p) (mk-Prod lzero lzero nat nat q r)) -> And lzero lzero (Not lzero (divides p r)) (eq lzero nat n (times (exp p q) r))
p-ord-to-exp1 = λ (p : nat) -> λ (n : nat) -> λ (q : nat) -> λ (r : nat) -> λ (lt1p : lt (S O) p) -> λ (posn : lt O n) -> λ (Hord : eq lzero (Prod lzero lzero nat nat) (p-ord n p) (mk-Prod lzero lzero nat nat q r)) -> conj lzero lzero (Not lzero (divides p r)) (eq lzero nat n (times (exp p q) r)) (not-to-not lzero (divides p r) (eq lzero nat (mod r p) O) (divides-to-mod-O p r (lt-to-le (S O) p lt1p)) (p-ord-aux-to-not-mod-O n n p q r lt1p posn (le-n n) Hord)) (p-ord-aux-to-exp n n p q r (lt-to-le (S O) p lt1p) Hord)
let-clause-10331'' : (p : nat) -> (n : nat) -> (n1 : nat) -> (q : nat) -> (p1 : nat) -> (p2 : nat) -> (qa : nat) -> (ra : nat) -> (H : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S (S p2))) (mk-Prod lzero lzero nat nat qa ra)) -> (x2515 : nat) -> (x2516 : nat) -> eq lzero nat x2515 (plus (times x2516 (div x2515 x2516)) (mod x2515 x2516))
let-clause-10331'' = λ (p : nat) -> λ (n : nat) -> λ (n1 : nat) -> λ (q : nat) -> λ (p1 : nat) -> λ (p2 : nat) -> λ (qa : nat) -> λ (ra : nat) -> λ (H : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S (S p2))) (mk-Prod lzero lzero nat nat qa ra)) -> λ (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)
eq-p-ord-q-O : (p : nat) -> (n : nat) -> (q : nat) -> (X-- : eq lzero (Prod lzero lzero nat nat) (p-ord n p) (mk-Prod lzero lzero nat nat q O)) -> And lzero lzero (eq lzero nat n O) (eq lzero nat q O)
eq-p-ord-q-O = λ (p : nat) -> λ (n : nat) -> match-nat lzero (λ (X-- : nat) -> (q : nat) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux X-- X-- p) (mk-Prod lzero lzero nat nat q O)) -> And lzero lzero (eq lzero nat X-- O) (eq lzero nat q O)) (λ (q : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux O O X--) (mk-Prod lzero lzero nat nat q O)) -> And lzero lzero (eq lzero nat O O) (eq lzero nat q O)) (λ (H : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O O) (mk-Prod lzero lzero nat nat q O)) -> Prod-discr lzero lzero lzero nat nat (mk-Prod lzero lzero nat nat O O) (mk-Prod lzero lzero nat nat q O) H (And lzero lzero (eq lzero nat O O) (eq lzero nat q O)) (λ (e0 : eq lzero nat (R0 lzero nat O) q) -> eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O O) (mk-Prod lzero lzero nat nat x-1 O)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) O x-1 X-x-2) O) -> And lzero lzero (eq lzero nat O O) (eq lzero nat x-1 O)) (λ (H0 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O O) (mk-Prod lzero lzero nat nat O O)) -> streicherK lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O O) (λ (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O O) (mk-Prod lzero lzero nat nat O O)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) O O (refl lzero nat O)) O) -> And lzero lzero (eq lzero nat O O) (eq lzero nat O O)) (λ (e00 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) O O (refl lzero nat O)) O) -> streicherK lzero lzero nat O (λ (X-- : eq lzero nat O O) -> And lzero lzero (eq lzero nat O O) (eq lzero nat O O)) (conj lzero lzero (eq lzero nat O O) (eq lzero nat O O) (refl lzero nat O) (refl lzero nat O)) e00) H0) q e0 H)) (λ (q1 : nat) -> λ (H : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O O) (mk-Prod lzero lzero nat nat q O)) -> Prod-discr lzero lzero lzero nat nat (mk-Prod lzero lzero nat nat O O) (mk-Prod lzero lzero nat nat q O) H (And lzero lzero (eq lzero nat O O) (eq lzero nat q O)) (λ (e0 : eq lzero nat (R0 lzero nat O) q) -> eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O O) (mk-Prod lzero lzero nat nat x-1 O)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) O x-1 X-x-2) O) -> And lzero lzero (eq lzero nat O O) (eq lzero nat x-1 O)) (λ (H0 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O O) (mk-Prod lzero lzero nat nat O O)) -> streicherK lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O O) (λ (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O O) (mk-Prod lzero lzero nat nat O O)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) O O (refl lzero nat O)) O) -> And lzero lzero (eq lzero nat O O) (eq lzero nat O O)) (λ (e00 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) O O (refl lzero nat O)) O) -> streicherK lzero lzero nat O (λ (X-- : eq lzero nat O O) -> And lzero lzero (eq lzero nat O O) (eq lzero nat O O)) (conj lzero lzero (eq lzero nat O O) (eq lzero nat O O) (refl lzero nat O) (refl lzero nat O)) e00) H0) q e0 H)) p) (λ (n1 : nat) -> λ (q : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) X--) (mk-Prod lzero lzero nat nat q O)) -> And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat q O)) (λ (H : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O (S n1)) (mk-Prod lzero lzero nat nat q O)) -> Prod-discr lzero lzero lzero nat nat (mk-Prod lzero lzero nat nat O (S n1)) (mk-Prod lzero lzero nat nat q O) H (And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat q O)) (λ (e0 : eq lzero nat (R0 lzero nat O) q) -> eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O (S n1)) (mk-Prod lzero lzero nat nat x-1 O)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) (S n1) x-1 X-x-2) O) -> And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat x-1 O)) (λ (H0 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O (S n1)) (mk-Prod lzero lzero nat nat O O)) -> λ (e00 : eq lzero nat (R1 lzero lzero nat O (λ (x0 : nat) -> λ (p0 : eq lzero nat O x0) -> nat) (S n1) O (refl lzero nat O)) O) -> nat-discr lzero (S n1) O e00 (And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat O O))) q e0 H)) (λ (p1 : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S X--)) (mk-Prod lzero lzero nat nat q O)) -> And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat q O)) (eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S n1) (S n1)) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat (S n1) (S n1))) -> (X--1 : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat q O)) -> And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat q O)) (λ (H : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S n1) (S n1)) (mk-Prod lzero lzero nat nat q O)) -> Prod-discr lzero lzero lzero nat nat (mk-Prod lzero lzero nat nat (S n1) (S n1)) (mk-Prod lzero lzero nat nat q O) H (And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat q O)) (λ (e0 : eq lzero nat (R0 lzero nat (S n1)) q) -> eq-ind lzero lzero nat (S n1) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S n1) x-1) -> (X-- : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S n1) (S n1)) (mk-Prod lzero lzero nat nat x-1 O)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat (S n1) (λ (x0 : nat) -> λ (p0 : eq lzero nat (S n1) x0) -> nat) (S n1) x-1 X-x-2) O) -> And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat x-1 O)) (λ (H0 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (S n1) (S n1)) (mk-Prod lzero lzero nat nat (S n1) O)) -> λ (e00 : eq lzero nat (R1 lzero lzero nat (S n1) (λ (x0 : nat) -> λ (p0 : eq lzero nat (S n1) x0) -> nat) (S n1) (S n1) (refl lzero nat (S n1))) O) -> nat-discr lzero (S n1) O e00 (And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat (S n1) O))) q e0 H)) (p-ord-aux (S n1) (S n1) (S O)) (p-ord-degenerate (S n1) (S n1))) (λ (p2 : nat) -> match-Prod lzero lzero nat nat lzero (λ (X-- : Prod lzero lzero nat nat) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S (S p2))) X--) -> (X--2 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S (S p2))) (mk-Prod lzero lzero nat nat q O)) -> And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat q O)) (λ (qa : nat) -> λ (ra : nat) -> λ (H : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S (S p2))) (mk-Prod lzero lzero nat nat qa ra)) -> match-And lzero lzero (Not lzero (divides (S (S p2)) ra)) (eq lzero nat (S n1) (times (exp (S (S p2)) qa) ra)) lzero (λ (X-- : And lzero lzero (Not lzero (divides (S (S p2)) ra)) (eq lzero nat (S n1) (times (exp (S (S p2)) qa) ra))) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S (S p2))) (mk-Prod lzero lzero nat nat q O)) -> And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat q O)) (λ (X-- : Not lzero (divides (S (S p2)) ra)) -> λ (H1 : eq lzero nat (S n1) (times (exp (S (S p2)) qa) ra)) -> eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat qa ra) (λ (x : Prod lzero lzero nat nat) -> λ (X-0 : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat qa ra)) -> (X--1 : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat q O)) -> And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat q O)) (λ (H2 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat qa ra) (mk-Prod lzero lzero nat nat q O)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> And lzero lzero (eq lzero nat (S n1) O) (eq lzero nat q O)) (Prod-discr lzero lzero lzero nat nat (mk-Prod lzero lzero nat nat qa ra) (mk-Prod lzero lzero nat nat q O) H2 (False lzero) (λ (e0 : eq lzero nat (R0 lzero nat qa) q) -> eq-ind-r lzero lzero nat q (λ (x : nat) -> λ (X-0 : eq lzero nat x q) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S (S p2))) (mk-Prod lzero lzero nat nat x ra)) -> (X--2 : eq lzero nat (S n1) (times (exp (S (S p2)) x) ra)) -> (X--3 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat x ra) (mk-Prod lzero lzero nat nat q O)) -> (X-e1 : eq lzero nat (R1 lzero lzero nat x (λ (x0 : nat) -> λ (p0 : eq lzero nat x x0) -> nat) ra q X-0) O) -> False lzero) (λ (H0 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S (S p2))) (mk-Prod lzero lzero nat nat q ra)) -> λ (H10 : eq lzero nat (S n1) (times (exp (S (S p2)) q) ra)) -> λ (H20 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat q ra) (mk-Prod lzero lzero nat nat q O)) -> λ (e00 : eq lzero nat (R1 lzero lzero nat q (λ (x0 : nat) -> λ (p0 : eq lzero nat q x0) -> nat) ra q (refl lzero nat q)) O) -> eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-0 : eq lzero nat x O) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S (S p2))) (mk-Prod lzero lzero nat nat q x)) -> (X--2 : eq lzero nat (S n1) (times (exp (S (S p2)) q) x)) -> (X--3 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat q x) (mk-Prod lzero lzero nat nat q O)) -> False lzero) (λ (H3 : eq lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S (S p2))) (mk-Prod lzero lzero nat nat q O)) -> λ (H11 : eq lzero nat (S n1) (times (exp (S (S p2)) q) O)) -> λ (H21 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat q O) (mk-Prod lzero lzero nat nat q O)) -> streicherK lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat q O) (λ (X--1 : eq lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat q O) (mk-Prod lzero lzero nat nat q O)) -> False lzero) (eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> (X--1 : eq lzero nat (S n1) x-1) -> False lzero) (λ (Habs : eq lzero nat (S n1) O) -> nat-discr lzero (S n1) O Habs (False lzero)) (times (exp (S (S p2)) q) O) (times-n-O (exp (S (S p2)) q)) H11) H21) ra e00 H0 H10 H20) qa e0 H H1 H2))) (p-ord-aux (S n1) (S n1) (S (S p2))) H) (p-ord-to-exp1 (S (S p2)) (S n1) qa ra (eq-coerc lzero (lt (mod (S O) O) (plus (plus (mod (S O) O) (times O (div (S O) O))) (S p2))) (lt (S O) (S (S p2))) (lt-plus-Sn-r (mod (S O) O) (times O (div (S O) O)) p2) (rewrite-l lzero (lsuc lzero) nat (S O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (mod (S O) O) (plus X-- (S p2))) (lt (S O) (S (S p2)))) (rewrite-l lzero (lsuc lzero) nat (S O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (plus (S O) (S p2))) (lt (S O) (S (S p2)))) (rewrite-r lzero (lsuc lzero) nat (S (S p2)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (S O) X--) (lt (S O) (S (S p2)))) (refl (lsuc lzero) (Set (lzero)) (lt (S O) (S (S p2)))) (plus (S O) (S p2)) (rewrite-r lzero lzero nat (times (S p2) (S O)) (λ (X-- : nat) -> eq lzero nat (plus (S O) X--) (S (S p2))) (rewrite-r lzero lzero nat (times (S (S p2)) (S O)) (λ (X-- : nat) -> eq lzero nat (plus (S O) (times (S p2) (S O))) X--) (times-Sn-m (S p2) (S O)) (S (S p2)) (times-n-1 (S (S p2)))) (S p2) (times-n-1 (S p2)))) (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'' p n n1 q p1 p2 qa ra H (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'' p n n1 q p1 p2 qa ra H (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-O-S n1) H)) (p-ord-aux (S n1) (S n1) (S (S p2))) (refl lzero (Prod lzero lzero nat nat) (p-ord-aux (S n1) (S n1) (S (S p2))))) p1) p) n
p-ord-times : (p : nat) -> (a : nat) -> (b : nat) -> (qa : nat) -> (ra : nat) -> (qb : nat) -> (rb : nat) -> (X-- : prime p) -> (X--1 : lt O a) -> (X--2 : lt O b) -> (X--3 : eq lzero (Prod lzero lzero nat nat) (p-ord a p) (mk-Prod lzero lzero nat nat qa ra)) -> (X--4 : eq lzero (Prod lzero lzero nat nat) (p-ord b p) (mk-Prod lzero lzero nat nat qb rb)) -> eq lzero (Prod lzero lzero nat nat) (p-ord (times a b) p) (mk-Prod lzero lzero nat nat (plus qa qb) (times ra rb))
p-ord-times = λ (p : nat) -> λ (a : nat) -> λ (b : nat) -> λ (qa : nat) -> λ (ra : nat) -> λ (qb : nat) -> λ (rb : nat) -> λ (Hprime : prime p) -> λ (posa : lt O a) -> λ (posb : lt O b) -> λ (porda : eq lzero (Prod lzero lzero nat nat) (p-ord a p) (mk-Prod lzero lzero nat nat qa ra)) -> λ (pordb : eq lzero (Prod lzero lzero nat nat) (p-ord b p) (mk-Prod lzero lzero nat nat qb rb)) -> match-And lzero lzero (Not lzero (divides p ra)) (eq lzero nat a (times (exp p qa) ra)) lzero (λ (X-- : And lzero lzero (Not lzero (divides p ra)) (eq lzero nat a (times (exp p qa) ra))) -> eq lzero (Prod lzero lzero nat nat) (p-ord (times a b) p) (mk-Prod lzero lzero nat nat (plus qa qb) (times ra rb))) (λ (Hdiva : Not lzero (divides p ra)) -> λ (Ha : eq lzero nat a (times (exp p qa) ra)) -> And-ind lzero lzero lzero (Not lzero (divides p rb)) (eq lzero nat b (times (exp p qb) rb)) (λ (X-x-118 : And lzero lzero (Not lzero (divides p rb)) (eq lzero nat b (times (exp p qb) rb))) -> eq lzero (Prod lzero lzero nat nat) (p-ord (times a b) p) (mk-Prod lzero lzero nat nat (plus qa qb) (times ra rb))) (λ (Hdivb : Not lzero (divides p rb)) -> λ (Hb : eq lzero nat b (times (exp p qb) rb)) -> p-ord-exp1 p (times a b) (plus qa qb) (times ra rb) (lt-to-le (S O) p (prime-to-lt-SO p Hprime)) (nmk lzero (divides p (times ra rb)) (λ (Hdiv : divides p (times ra rb)) -> match-Or lzero lzero (divides p ra) (divides p rb) lzero (λ (X-- : Or lzero lzero (divides p ra) (divides p rb)) -> False lzero) (λ (Habs : divides p ra) -> absurd lzero (divides p ra) Habs Hdiva) (λ (Habs : divides p rb) -> absurd lzero (divides p rb) Habs Hdivb) (divides-times-to-divides p ra rb Hprime Hdiv))) (eq-ind-r lzero lzero nat (times (exp p qa) ra) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p qa) ra)) -> eq lzero nat (times x b) (times (exp p (plus qa qb)) (times ra rb))) (eq-ind-r lzero lzero nat (times (exp p qb) rb) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p qb) rb)) -> eq lzero nat (times (times (exp p qa) ra) x) (times (exp p (plus qa qb)) (times ra rb))) (rewrite-r lzero lzero nat (times ra (exp p qa)) (λ (X-- : nat) -> eq lzero nat (times X-- (times (exp p qb) rb)) (times (exp p (plus qa qb)) (times ra rb))) (rewrite-r lzero lzero nat (times rb (exp p qb)) (λ (X-- : nat) -> eq lzero nat (times (times ra (exp p qa)) X--) (times (exp p (plus qa qb)) (times ra rb))) (rewrite-r lzero lzero nat (times ra (times (exp p qa) (times rb (exp p qb)))) (λ (X-- : nat) -> eq lzero nat X-- (times (exp p (plus qa qb)) (times ra rb))) (rewrite-r lzero lzero nat (times rb (times (exp p qa) (exp p qb))) (λ (X-- : nat) -> eq lzero nat (times ra X--) (times (exp p (plus qa qb)) (times ra rb))) (rewrite-r lzero lzero nat (times (exp p qa) (exp p qb)) (λ (X-- : nat) -> eq lzero nat (times ra (times rb (times (exp p qa) (exp p qb)))) (times X-- (times ra rb))) (rewrite-r lzero lzero nat (times (times ra rb) (times (exp p qa) (exp p qb))) (λ (X-- : nat) -> eq lzero nat (times ra (times rb (times (exp p qa) (exp p qb)))) X--) (rewrite-r lzero lzero nat (times ra (times rb (times (exp p qa) (exp p qb)))) (λ (X-- : nat) -> eq lzero nat (times ra (times rb (times (exp p qa) (exp p qb)))) X--) (refl lzero nat (times ra (times rb (times (exp p qa) (exp p qb))))) (times (times ra rb) (times (exp p qa) (exp p qb))) (associative-times ra rb (times (exp p qa) (exp p qb)))) (times (times (exp p qa) (exp p qb)) (times ra rb)) (commutative-times (times (exp p qa) (exp p qb)) (times ra rb))) (exp p (plus qa qb)) (exp-plus-times p qa qb)) (times (exp p qa) (times rb (exp p qb))) (times-times (exp p qa) rb (exp p qb))) (times (times ra (exp p qa)) (times rb (exp p qb))) (associative-times ra (exp p qa) (times rb (exp p qb)))) (times (exp p qb) rb) (commutative-times (exp p qb) rb)) (times (exp p qa) ra) (commutative-times (exp p qa) ra)) b Hb) a Ha)) (p-ord-to-exp1 p b qb rb (prime-to-lt-SO p Hprime) posb pordb)) (p-ord-to-exp1 p a qa ra (prime-to-lt-SO p Hprime) posa porda)
fst-p-ord-times : (p : nat) -> (a : nat) -> (b : nat) -> (X-- : prime p) -> (X--1 : lt O a) -> (X--2 : lt O b) -> eq lzero nat (fst lzero lzero nat nat (p-ord (times a b) p)) (plus (fst lzero lzero nat nat (p-ord a p)) (fst lzero lzero nat nat (p-ord b p)))
fst-p-ord-times = λ (p : nat) -> λ (a : nat) -> λ (b : nat) -> λ (primep : prime p) -> λ (posa : lt O a) -> λ (posb : lt O b) -> eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat (plus (fst lzero lzero nat nat (p-ord a p)) (fst lzero lzero nat nat (p-ord b p))) (times (snd lzero lzero nat nat (p-ord a p)) (snd lzero lzero nat nat (p-ord b p)))) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat (plus (fst lzero lzero nat nat (p-ord a p)) (fst lzero lzero nat nat (p-ord b p))) (times (snd lzero lzero nat nat (p-ord a p)) (snd lzero lzero nat nat (p-ord b p))))) -> eq lzero nat (fst lzero lzero nat nat x) (plus (fst lzero lzero nat nat (p-ord a p)) (fst lzero lzero nat nat (p-ord b p)))) (refl lzero nat (plus (fst lzero lzero nat nat (p-ord a p)) (fst lzero lzero nat nat (p-ord b p)))) (p-ord (times a b) p) (p-ord-times p a b (fst lzero lzero nat nat (p-ord a p)) (snd lzero lzero nat nat (p-ord a p)) (fst lzero lzero nat nat (p-ord b p)) (snd lzero lzero nat nat (p-ord b p)) primep posa posb (rewrite-l lzero lzero (Prod lzero lzero nat nat) (p-ord a p) (λ (X-- : Prod lzero lzero nat nat) -> eq lzero (Prod lzero lzero nat nat) (p-ord a p) X--) (refl lzero (Prod lzero lzero nat nat) (p-ord a p)) (mk-Prod lzero lzero nat nat (fst lzero lzero nat nat (p-ord a p)) (snd lzero lzero nat nat (p-ord a p))) (eq-pair-fst-snd lzero lzero nat nat (p-ord a p))) (rewrite-l lzero lzero (Prod lzero lzero nat nat) (p-ord b p) (λ (X-- : Prod lzero lzero nat nat) -> eq lzero (Prod lzero lzero nat nat) (p-ord b p) X--) (refl lzero (Prod lzero lzero nat nat) (p-ord b p)) (mk-Prod lzero lzero nat nat (fst lzero lzero nat nat (p-ord b p)) (snd lzero lzero nat nat (p-ord b p))) (eq-pair-fst-snd lzero lzero nat nat (p-ord b p))))
p-ord-p : (p : nat) -> (X-- : lt (S O) p) -> eq lzero (Prod lzero lzero nat nat) (p-ord p p) (mk-Prod lzero lzero nat nat (S O) (S O))
p-ord-p = λ (p : nat) -> λ (ltp1 : lt (S O) p) -> p-ord-exp1 p p (S O) (S O) (lt-to-le (S O) p ltp1) (nmk lzero (divides p (S O)) (λ (divp1 : divides p (S O)) -> absurd lzero (lt (S O) p) ltp1 (le-to-not-lt p (S O) (divides-to-le p (S O) (lt-O-S O) divp1)))) (rewrite-l lzero lzero nat p (λ (X-- : nat) -> eq lzero nat p (times X-- (S O))) (rewrite-l lzero lzero nat (plus p (times p O)) (λ (X-- : nat) -> eq lzero nat p X--) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat p (plus p X--)) (rewrite-l lzero lzero nat p (λ (X-- : nat) -> eq lzero nat p X--) (refl lzero nat p) (plus p O) (plus-n-O p)) (times p O) (times-n-O p)) (times p (S O)) (times-n-Sm p O)) (exp p (S O)) (exp-n-1 p))
divides-to-p-ord : (p : nat) -> (a : nat) -> (b : nat) -> (c : nat) -> (d : nat) -> (n : nat) -> (m : nat) -> (X-- : lt O n) -> (X--1 : lt O m) -> (X--2 : prime p) -> (X--3 : divides n m) -> (X--4 : eq lzero (Prod lzero lzero nat nat) (p-ord n p) (mk-Prod lzero lzero nat nat a b)) -> (X--5 : eq lzero (Prod lzero lzero nat nat) (p-ord m p) (mk-Prod lzero lzero nat nat c d)) -> And lzero lzero (divides b d) (le a c)
divides-to-p-ord = λ (p : nat) -> λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (d : nat) -> λ (n : nat) -> λ (m : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (primep : prime p) -> λ (divnm : divides n m) -> λ (ordn : eq lzero (Prod lzero lzero nat nat) (p-ord n p) (mk-Prod lzero lzero nat nat a b)) -> λ (ordm : eq lzero (Prod lzero lzero nat nat) (p-ord m p) (mk-Prod lzero lzero nat nat c d)) -> match-And lzero lzero (Not lzero (divides p b)) (eq lzero nat n (times (exp p a) b)) lzero (λ (X-- : And lzero lzero (Not lzero (divides p b)) (eq lzero nat n (times (exp p a) b))) -> And lzero lzero (divides b d) (le a c)) (λ (divn : Not lzero (divides p b)) -> λ (eqn : eq lzero nat n (times (exp p a) b)) -> match-And lzero lzero (Not lzero (divides p d)) (eq lzero nat m (times (exp p c) d)) lzero (λ (X-- : And lzero lzero (Not lzero (divides p d)) (eq lzero nat m (times (exp p c) d))) -> And lzero lzero (divides b d) (le a c)) (λ (divm : Not lzero (divides p d)) -> λ (eqm : eq lzero nat m (times (exp p c) d)) -> conj lzero lzero (divides b d) (le a c) (gcd-1-to-divides-times-to-divides b (exp p c) d (match-Or lzero lzero (lt O b) (eq lzero nat O b) lzero (λ (X-- : Or lzero lzero (lt O b) (eq lzero nat O b)) -> lt O b) (λ (auto : lt O b) -> auto) (λ (auto : eq lzero nat O b) -> eq-coerc lzero (lt O n) (lt O b) posn (rewrite-r lzero (lsuc lzero) nat b (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- n) (lt O b)) (rewrite-r lzero (lsuc lzero) nat b (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt b X--) (lt O b)) (rewrite-r lzero (lsuc lzero) nat b (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt b b) (lt X-- b)) (refl (lsuc lzero) (Set (lzero)) (lt b b)) O auto) n (rewrite-r lzero lzero nat (times b (exp p a)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times (exp p a) b) (λ (X-- : nat) -> eq lzero nat n X--) eqn (times b (exp p a)) (commutative-times (exp p a) b)) b (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat b (times X-- (exp p a))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat X-- (times O (exp p a))) (times-O-n (exp p a)) b auto) b auto))) O auto)) (le-to-or-lt-eq O b (le-O-n b))) (nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat (gcd b (exp p X-x-365)) (S O)) (eq-ind-r lzero lzero nat (gcd (exp p O) b) (λ (x : nat) -> λ (X-- : eq lzero nat x (gcd (exp p O) b)) -> eq lzero nat x (S O)) (rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (refl lzero nat (S O)) (gcd (exp p O) b) (rewrite-l lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (gcd X-- b) (S O)) (gcd-SO-n b) (exp p O) (exp-n-O p))) (gcd b (exp p O)) (commutative-gcd b (exp p O))) (λ (c0 : nat) -> λ (Hind : eq lzero nat (gcd b (exp p c0)) (S O)) -> eq-gcd-times-1 b (exp p c0) p (lt-O-exp p c0 (lt-to-le (S O) p (prime-to-lt-SO p primep))) (lt-to-le (S O) p (prime-to-lt-SO p primep)) Hind (eq-ind-r lzero lzero nat (gcd p b) (λ (x : nat) -> λ (X-- : eq lzero nat x (gcd p b)) -> eq lzero nat x (S O)) (prime-to-gcd-1 p b primep divn) (gcd b p) (commutative-gcd b p))) c) (transitive-divides b n (times (exp p c) d) (quotient b n (exp p a) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) (times b (exp p a)) (rewrite-l lzero lzero nat (times (exp p a) b) (λ (X-- : nat) -> eq lzero nat n X--) eqn (times b (exp p a)) (commutative-times (exp p a) b)))) (eq-ind lzero lzero nat m (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat m x-1) -> divides n x-1) divnm (times (exp p c) d) eqm))) (le-exp-to-le p a c (prime-to-lt-SO p primep) (divides-to-le (exp p a) (exp p c) (lt-O-exp p c (lt-to-le (S O) p (prime-to-lt-SO p primep))) (gcd-1-to-divides-times-to-divides (exp p a) d (exp p c) (lt-O-exp p a (lt-to-le (S O) p (prime-to-lt-SO p primep))) (nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat (gcd (exp p X-x-365) d) (S O)) (gcd-SO-n d) (λ (a0 : nat) -> λ (Hind : eq lzero nat (gcd (exp p a0) d) (S O)) -> eq-ind-r lzero lzero nat (gcd d (times (exp p a0) p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (gcd d (times (exp p a0) p))) -> eq lzero nat x (S O)) (eq-gcd-times-1 d (exp p a0) p (lt-O-exp p a0 (lt-to-le (S O) p (prime-to-lt-SO p primep))) (lt-to-le (S O) p (prime-to-lt-SO p primep)) (rewrite-l lzero lzero nat (gcd d (exp p a0)) (λ (X-- : nat) -> eq lzero nat (gcd d (exp p a0)) X--) (refl lzero nat (gcd d (exp p a0))) (S O) (rewrite-l lzero lzero nat (gcd (exp p a0) d) (λ (X-- : nat) -> eq lzero nat X-- (S O)) Hind (gcd d (exp p a0)) (commutative-gcd (exp p a0) d))) (eq-ind-r lzero lzero nat (gcd p d) (λ (x : nat) -> λ (X-- : eq lzero nat x (gcd p d)) -> eq lzero nat x (S O)) (prime-to-gcd-1 p d primep divm) (gcd d p) (commutative-gcd d p))) (gcd (times (exp p a0) p) d) (commutative-gcd (times (exp p a0) p) d)) a) (transitive-divides (exp p a) n (times d (exp p c)) (quotient (exp p a) n b (rewrite-r lzero lzero nat (times b (exp p a)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) (times b (exp p a)) (rewrite-l lzero lzero nat (times (exp p a) b) (λ (X-- : nat) -> eq lzero nat n X--) eqn (times b (exp p a)) (commutative-times (exp p a) b))) (times (exp p a) b) (commutative-times (exp p a) b))) (eq-coerc lzero (divides n m) (divides n (times d (exp p c))) divnm (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (divides n m) (divides n X--)) (refl (lsuc lzero) (Set (lzero)) (divides n m)) (times d (exp p c)) (rewrite-l lzero lzero nat (times (exp p c) d) (λ (X-- : nat) -> eq lzero nat m X--) eqm (times d (exp p c)) (commutative-times (exp p c) d))))))))) (p-ord-to-exp1 p m c d (prime-to-lt-SO p primep) posm ordm)) (p-ord-to-exp1 p n a b (prime-to-lt-SO p primep) posn ordn)
not-divides-to-p-ord-O : (n : nat) -> (i : nat) -> (X-- : Not lzero (divides (nth-prime i) n)) -> eq lzero (Prod lzero lzero nat nat) (p-ord n (nth-prime i)) (mk-Prod lzero lzero nat nat O n)
not-divides-to-p-ord-O = λ (n : nat) -> λ (i : nat) -> λ (H : Not lzero (divides (nth-prime i) n)) -> p-ord-exp1 (nth-prime i) n O n (lt-O-nth-prime-n i) H (rewrite-r lzero lzero nat (times (exp (nth-prime i) O) n) (λ (X-- : nat) -> eq lzero nat X-- (times (exp (nth-prime i) O) n)) (refl lzero nat (times (exp (nth-prime i) O) n)) n (rewrite-r lzero lzero nat (plus n O) (λ (X-- : nat) -> eq lzero nat X-- (times (exp (nth-prime i) O) n)) (rewrite-r lzero lzero nat (times O n) (λ (X-- : nat) -> eq lzero nat (plus n X--) (times (exp (nth-prime i) O) n)) (rewrite-l lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (plus n (times O n)) (times X-- n)) (times-Sn-m O n) (exp (nth-prime i) O) (exp-n-O (nth-prime i))) O (times-O-n n)) n (plus-n-O n)))
p-ord-O-to-not-divides : (n : nat) -> (i : nat) -> (r : nat) -> (X-- : lt O n) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord n (nth-prime i)) (mk-Prod lzero lzero nat nat O r)) -> Not lzero (divides (nth-prime i) n)
p-ord-O-to-not-divides = λ (n : nat) -> λ (i : nat) -> λ (r : nat) -> λ (posn : lt O n) -> λ (Hord : eq lzero (Prod lzero lzero nat nat) (p-ord n (nth-prime i)) (mk-Prod lzero lzero nat nat O r)) -> match-And lzero lzero (Not lzero (divides (nth-prime i) r)) (eq lzero nat n (times (exp (nth-prime i) O) r)) lzero (λ (X-- : And lzero lzero (Not lzero (divides (nth-prime i) r)) (eq lzero nat n (times (exp (nth-prime i) O) r))) -> Not lzero (divides (nth-prime i) n)) (λ (H : Not lzero (divides (nth-prime i) r)) -> eq-ind lzero lzero nat r (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat r x-1) -> (X-- : eq lzero nat n x-1) -> Not lzero (divides (nth-prime i) n)) (λ (auto : eq lzero nat n r) -> eq-coerc lzero (Not lzero (divides (nth-prime i) r)) (Not lzero (divides (nth-prime i) n)) H (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (Not lzero (divides (nth-prime i) X--)) (Not lzero (divides (nth-prime i) n))) (refl (lsuc lzero) (Set (lzero)) (Not lzero (divides (nth-prime i) n))) r auto)) (plus r O) (plus-n-O r)) (p-ord-to-exp1 (nth-prime i) n O r (lt-SO-nth-prime-n i) posn Hord)
p-ord-to-not-eq-O : (n : nat) -> (p : nat) -> (q : nat) -> (r : nat) -> (X-- : lt (S O) n) -> (X--1 : eq lzero (Prod lzero lzero nat nat) (p-ord n (nth-prime p)) (mk-Prod lzero lzero nat nat q r)) -> Not lzero (eq lzero nat r O)
p-ord-to-not-eq-O = λ (n : nat) -> λ (p : nat) -> λ (q : nat) -> λ (r : nat) -> λ (lt1n : lt (S O) n) -> λ (Hord : eq lzero (Prod lzero lzero nat nat) (p-ord n (nth-prime p)) (mk-Prod lzero lzero nat nat q r)) -> match-And lzero lzero (Not lzero (divides (nth-prime p) r)) (eq lzero nat n (times (exp (nth-prime p) q) r)) lzero (λ (X-- : And lzero lzero (Not lzero (divides (nth-prime p) r)) (eq lzero nat n (times (exp (nth-prime p) q) r))) -> Not lzero (eq lzero nat r O)) (λ (H1 : Not lzero (divides (nth-prime p) r)) -> λ (H2 : eq lzero nat n (times (exp (nth-prime p) q) r)) -> not-to-not lzero (eq lzero nat r O) (eq lzero nat O n) (λ (eqr : eq lzero nat r O) -> eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> (X--1 : eq lzero nat n (times (exp (nth-prime p) q) x)) -> eq lzero nat O n) (λ (auto : eq lzero nat n (times (exp (nth-prime p) q) O)) -> rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat X-- n) (refl lzero nat n) O (rewrite-r lzero lzero nat (times O (exp (nth-prime p) q)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times (exp (nth-prime p) q) O) (λ (X-- : nat) -> eq lzero nat n X--) auto (times O (exp (nth-prime p) q)) (commutative-times (exp (nth-prime p) q) O)) O (times-O-n (exp (nth-prime p) q)))) r eqr H2) (lt-to-not-eq O n (lt-to-le (S O) n lt1n))) (p-ord-to-exp1 (nth-prime p) n q r (lt-SO-nth-prime-n p) (lt-to-le (S O) n lt1n) Hord)
ord : (X-- : nat) -> (X--1 : nat) -> nat
ord = λ (n : nat) -> λ (p : nat) -> fst lzero lzero nat nat (p-ord n p)
ord-rem : (X-- : nat) -> (X--1 : nat) -> nat
ord-rem = λ (n : nat) -> λ (p : nat) -> snd lzero lzero nat nat (p-ord n p)
ord-eq : (n : nat) -> (p : nat) -> eq lzero nat (ord n p) (fst lzero lzero nat nat (p-ord n p))
ord-eq = λ (n : nat) -> λ (p : nat) -> refl lzero nat (ord n p)
ord-rem-eq : (n : nat) -> (p : nat) -> eq lzero nat (ord-rem n p) (snd lzero lzero nat nat (p-ord n p))
ord-rem-eq = λ (n : nat) -> λ (p : nat) -> refl lzero nat (ord-rem n p)
divides-to-ord : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : lt O n) -> (X--1 : lt O m) -> (X--2 : prime p) -> (X--3 : divides n m) -> And lzero lzero (divides (ord-rem n p) (ord-rem m p)) (le (ord n p) (ord m p))
divides-to-ord = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (H : lt O n) -> λ (H1 : lt O m) -> λ (H2 : prime p) -> λ (H3 : divides n m) -> divides-to-p-ord p (ord n p) (ord-rem n p) (ord m p) (ord-rem m p) n m H H1 H2 H3 (eq-pair-fst-snd lzero lzero nat nat (p-ord n p)) (eq-pair-fst-snd lzero lzero nat nat (p-ord m p))
divides-to-divides-ord-rem : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : lt O n) -> (X--1 : lt O m) -> (X--2 : prime p) -> (X--3 : divides n m) -> divides (ord-rem n p) (ord-rem m p)
divides-to-divides-ord-rem = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (H : lt O n) -> λ (H1 : lt O m) -> λ (H2 : prime p) -> λ (H3 : divides n m) -> match-And lzero lzero (divides (ord-rem n p) (ord-rem m p)) (le (ord n p) (ord m p)) lzero (λ (X-- : And lzero lzero (divides (ord-rem n p) (ord-rem m p)) (le (ord n p) (ord m p))) -> divides (ord-rem n p) (ord-rem m p)) (λ (auto : divides (ord-rem n p) (ord-rem m p)) -> λ (auto' : le (ord n p) (ord m p)) -> auto) (divides-to-ord p n m H H1 H2 H3)
divides-to-le-ord : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : lt O n) -> (X--1 : lt O m) -> (X--2 : prime p) -> (X--3 : divides n m) -> le (ord n p) (ord m p)
divides-to-le-ord = λ (p : nat) -> λ (n : nat) -> λ (m : nat) -> λ (H : lt O n) -> λ (H1 : lt O m) -> λ (H2 : prime p) -> λ (H3 : divides n m) -> match-And lzero lzero (divides (ord-rem n p) (ord-rem m p)) (le (ord n p) (ord m p)) lzero (λ (X-- : And lzero lzero (divides (ord-rem n p) (ord-rem m p)) (le (ord n p) (ord m p))) -> le (ord n p) (ord m p)) (λ (auto : divides (ord-rem n p) (ord-rem m p)) -> λ (auto' : le (ord n p) (ord m p)) -> auto') (divides-to-ord p n m H H1 H2 H3)
exp-ord : (p : nat) -> (n : nat) -> (X-- : lt (S O) p) -> (X--1 : lt O n) -> eq lzero nat n (times (exp p (ord n p)) (ord-rem n p))
exp-ord = λ (p : nat) -> λ (n : nat) -> λ (H : lt (S O) p) -> λ (H1 : lt O n) -> match-And lzero lzero (Not lzero (divides p (ord-rem n p))) (eq lzero nat n (times (exp p (ord n p)) (ord-rem n p))) lzero (λ (X-- : And lzero lzero (Not lzero (divides p (ord-rem n p))) (eq lzero nat n (times (exp p (ord n p)) (ord-rem n p)))) -> eq lzero nat n (times (exp p (ord n p)) (ord-rem n p))) (λ (auto : Not lzero (divides p (ord-rem n p))) -> λ (auto' : eq lzero nat n (times (exp p (ord n p)) (ord-rem n p))) -> rewrite-r lzero lzero nat (times (ord-rem n p) (exp p (ord n p))) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) (times (ord-rem n p) (exp p (ord n p))) (rewrite-l lzero lzero nat (times (exp p (ord n p)) (ord-rem n p)) (λ (X-- : nat) -> eq lzero nat n X--) auto' (times (ord-rem n p) (exp p (ord n p))) (commutative-times (exp p (ord n p)) (ord-rem n p)))) (times (exp p (ord n p)) (ord-rem n p)) (commutative-times (exp p (ord n p)) (ord-rem n p))) (p-ord-to-exp1 p n (ord n p) (ord-rem n p) H H1 (eq-pair-fst-snd lzero lzero nat nat (p-ord n p)))
divides-ord-rem : (p : nat) -> (n : nat) -> (X-- : lt (S O) p) -> (X--1 : lt O n) -> divides (ord-rem n p) n
divides-ord-rem = λ (p : nat) -> λ (n : nat) -> λ (H : lt (S O) p) -> λ (H1 : lt O n) -> quotient (ord-rem n p) n (exp p (ord n p)) (eq-ind-r lzero lzero nat (times (exp p (ord n p)) (ord-rem n p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p (ord n p)) (ord-rem n p))) -> eq lzero nat n x) (exp-ord p n H H1) (times (ord-rem n p) (exp p (ord n p))) (commutative-times (ord-rem n p) (exp p (ord n p))))
lt-O-ord-rem : (p : nat) -> (n : nat) -> (X-- : lt (S O) p) -> (X--1 : lt O n) -> lt O (ord-rem n p)
lt-O-ord-rem = λ (p : nat) -> λ (n : nat) -> λ (H : lt (S O) p) -> λ (H1 : lt O n) -> match-Or lzero lzero (lt O (ord-rem n p)) (eq lzero nat O (ord-rem n p)) lzero (λ (X-- : Or lzero lzero (lt O (ord-rem n p)) (eq lzero nat O (ord-rem n p))) -> lt O (ord-rem n p)) (λ (auto : lt O (ord-rem n p)) -> auto) (λ (remO : eq lzero nat O (ord-rem n p)) -> eq-ind lzero lzero nat O (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat O x-1) -> (X-- : divides x-1 n) -> lt O x-1) (λ (Hdiv0 : divides O n) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt O O) (absurd lzero (eq lzero nat O n) (match-divides O n lzero (λ (X-- : divides O n) -> eq lzero nat O n) (λ (q : nat) -> λ (auto : eq lzero nat n (times O q)) -> rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat X-- n) (refl lzero nat n) O (rewrite-r lzero lzero nat (times q O) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times O q) (λ (X-- : nat) -> eq lzero nat n X--) auto (times q O) (commutative-times O q)) O (times-n-O q))) Hdiv0) (lt-to-not-eq O n H1))) (ord-rem n p) remO (divides-ord-rem p n H H1)) (le-to-or-lt-eq O (ord-rem n p) (le-O-n (ord-rem n p)))
ord-times : (p : nat) -> (m : nat) -> (n : nat) -> (X-- : lt O m) -> (X--1 : lt O n) -> (X--2 : prime p) -> eq lzero nat (ord (times m n) p) (plus (ord m p) (ord n p))
ord-times = λ (p : nat) -> λ (m : nat) -> λ (n : nat) -> λ (H : lt O m) -> λ (H1 : lt O n) -> λ (H2 : prime p) -> eq-f lzero lzero (Prod lzero lzero nat nat) nat (fst lzero lzero nat nat) (p-ord (times m n) p) (mk-Prod lzero lzero nat nat (plus (ord m p) (ord n p)) (times (ord-rem m p) (ord-rem n p))) (p-ord-times p m n (ord m p) (ord-rem m p) (ord n p) (ord-rem n p) H2 H H1 (eq-pair-fst-snd lzero lzero nat nat (p-ord m p)) (eq-pair-fst-snd lzero lzero nat nat (p-ord n p)))
ord-exp : (p : nat) -> (m : nat) -> (X-- : lt (S O) p) -> eq lzero nat (ord (exp p m) p) m
ord-exp = λ (p : nat) -> λ (m : nat) -> λ (H : lt (S O) p) -> eq-ind-r lzero lzero nat (fst lzero lzero nat nat (p-ord (exp p m) p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (fst lzero lzero nat nat (p-ord (exp p m) p))) -> eq lzero nat x m) (eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat m (S O)) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat m (S O))) -> eq lzero nat (fst lzero lzero nat nat x) m) (refl lzero nat m) (p-ord (exp p m) p) (p-ord-exp1 p (exp p m) m (S O) (lt-to-le (S O) p H) (not-to-not lzero (divides p (S O)) (le p (S O)) (divides-to-le p (S O) (lt-O-S O)) (lt-to-not-le (S O) p H)) (rewrite-l lzero lzero nat (plus (exp p m) (times (exp p m) O)) (λ (X-- : nat) -> eq lzero nat (exp p m) X--) (rewrite-r lzero lzero nat (times O (exp p m)) (λ (X-- : nat) -> eq lzero nat (exp p m) (plus (exp p m) X--)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (exp p m) (plus (exp p m) X--)) (rewrite-r lzero lzero nat (plus O (exp p m)) (λ (X-- : nat) -> eq lzero nat (exp p m) X--) (rewrite-l lzero lzero nat (exp p m) (λ (X-- : nat) -> eq lzero nat (exp p m) X--) (refl lzero nat (exp p m)) (plus O (exp p m)) (plus-O-n (exp p m))) (plus (exp p m) O) (commutative-plus (exp p m) O)) (times O (exp p m)) (times-O-n (exp p m))) (times (exp p m) O) (commutative-times (exp p m) O)) (times (exp p m) (S O)) (times-n-Sm (exp p m) O)))) (ord (exp p m) p) (ord-eq (exp p m) p)
not-divides-to-ord-O : (p : nat) -> (m : nat) -> (X-- : prime p) -> (X--1 : Not lzero (divides p m)) -> eq lzero nat (ord m p) O
not-divides-to-ord-O = λ (p : nat) -> λ (m : nat) -> λ (H : prime p) -> λ (H1 : Not lzero (divides p m)) -> eq-ind-r lzero lzero nat (fst lzero lzero nat nat (p-ord m p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (fst lzero lzero nat nat (p-ord m p))) -> eq lzero nat x O) (eq-ind-r lzero lzero (Prod lzero lzero nat nat) (mk-Prod lzero lzero nat nat O m) (λ (x : Prod lzero lzero nat nat) -> λ (X-- : eq lzero (Prod lzero lzero nat nat) x (mk-Prod lzero lzero nat nat O m)) -> eq lzero nat (fst lzero lzero nat nat x) O) (refl lzero nat O) (p-ord m p) (p-ord-exp1 p m O m (prime-to-lt-O p H) H1 (rewrite-r lzero lzero nat (times (exp p O) m) (λ (X-- : nat) -> eq lzero nat X-- (times (exp p O) m)) (refl lzero nat (times (exp p O) m)) m (rewrite-r lzero lzero nat (plus m O) (λ (X-- : nat) -> eq lzero nat X-- (times (exp p O) m)) (rewrite-r lzero lzero nat (times O m) (λ (X-- : nat) -> eq lzero nat (plus m X--) (times (exp p O) m)) (rewrite-l lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (plus m (times O m)) (times X-- m)) (times-Sn-m O m) (exp p O) (exp-n-O p)) O (times-O-n m)) m (plus-n-O m))))) (ord m p) (ord-eq m p)
ord-O-to-not-divides : (p : nat) -> (m : nat) -> (X-- : lt O m) -> (X--1 : prime p) -> (X--2 : eq lzero nat (ord m p) O) -> Not lzero (divides p m)
ord-O-to-not-divides = λ (p : nat) -> λ (m : nat) -> λ (H : lt O m) -> λ (H1 : prime p) -> λ (H2 : eq lzero nat (ord m p) O) -> match-And lzero lzero (Not lzero (divides p (ord-rem m p))) (eq lzero nat m (times (exp p (ord m p)) (ord-rem m p))) lzero (λ (X-- : And lzero lzero (Not lzero (divides p (ord-rem m p))) (eq lzero nat m (times (exp p (ord m p)) (ord-rem m p)))) -> Not lzero (divides p m)) (λ (H3 : Not lzero (divides p (ord-rem m p))) -> eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> (X--1 : eq lzero nat m (times (exp p x) (ord-rem m p))) -> Not lzero (divides p m)) (eq-ind-r lzero lzero nat (times (ord-rem m p) (exp p O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (ord-rem m p) (exp p O))) -> (X--1 : eq lzero nat m x) -> Not lzero (divides p m)) (eq-ind lzero lzero nat (ord-rem m p) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (ord-rem m p) x-1) -> (X-- : eq lzero nat m x-1) -> Not lzero (divides p m)) (λ (auto : eq lzero nat m (ord-rem m p)) -> eq-coerc lzero (Not lzero (divides p (ord-rem m p))) (Not lzero (divides p m)) H3 (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (Not lzero (divides p X--)) (Not lzero (divides p m))) (refl (lsuc lzero) (Set (lzero)) (Not lzero (divides p m))) (ord-rem m p) auto)) (times (ord-rem m p) (S O)) (times-n-1 (ord-rem m p))) (times (exp p O) (ord-rem m p)) (commutative-times (exp p O) (ord-rem m p))) (ord m p) H2) (p-ord-to-exp1 p m (ord m p) (ord-rem m p) (prime-to-lt-SO p H1) H (eq-pair-fst-snd lzero lzero nat nat (p-ord m p)))
divides-to-not-ord-O : (p : nat) -> (m : nat) -> (X-- : lt O m) -> (X--1 : prime p) -> (X--2 : divides p m) -> Not lzero (eq lzero nat (ord m p) O)
divides-to-not-ord-O = λ (p : nat) -> λ (m : nat) -> λ (H : lt O m) -> λ (H1 : prime p) -> λ (H2 : divides p m) -> nmk lzero (eq lzero nat (ord m p) O) (λ (H3 : eq lzero nat (ord m p) O) -> absurd lzero (divides p m) H2 (ord-O-to-not-divides p m H H1 H3))
not-ord-O-to-divides : (p : nat) -> (m : nat) -> (X-- : lt O m) -> (X--1 : prime p) -> (X--2 : Not lzero (eq lzero nat (ord m p) O)) -> divides p m
not-ord-O-to-divides = λ (p : nat) -> λ (m : nat) -> λ (H : lt O m) -> λ (H1 : prime p) -> λ (H2 : Not lzero (eq lzero nat (ord m p) O)) -> eq-ind-r lzero lzero nat (times (exp p (ord m p)) (ord-rem m p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p (ord m p)) (ord-rem m p))) -> divides p x) (transitive-divides p (exp p (ord m p)) (times (exp p (ord m p)) (ord-rem m p)) (match-nat lzero (λ (X-- : nat) -> (X--1 : Not lzero (eq lzero nat X-- O)) -> divides p (exp p X--)) (λ (X-clearme : Not lzero (eq lzero nat O O)) -> match-Not lzero (eq lzero nat O O) lzero (λ (X-- : Not lzero (eq lzero nat O O)) -> divides p (exp p O)) (λ (H3 : (X-- : eq lzero nat O O) -> False lzero) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> divides p (exp p O)) (H3 (refl lzero nat O))) X-clearme) (λ (a : nat) -> λ (X-- : Not lzero (eq lzero nat (S a) O)) -> quotient p (times (exp p a) p) (exp p a) (rewrite-r lzero lzero nat (times p (exp p a)) (λ (X--1 : nat) -> eq lzero nat X--1 (times p (exp p a))) (refl lzero nat (times p (exp p a))) (times (exp p a) p) (commutative-times (exp p a) p))) (ord m p) H2) (quotient (exp p (ord m p)) (times (exp p (ord m p)) (ord-rem m p)) (ord-rem m p) (rewrite-r lzero lzero nat (times (ord-rem m p) (exp p (ord m p))) (λ (X-- : nat) -> eq lzero nat X-- (times (exp p (ord m p)) (ord-rem m p))) (rewrite-r lzero lzero nat (times (ord-rem m p) (exp p (ord m p))) (λ (X-- : nat) -> eq lzero nat (times (ord-rem m p) (exp p (ord m p))) X--) (refl lzero nat (times (ord-rem m p) (exp p (ord m p)))) (times (exp p (ord m p)) (ord-rem m p)) (commutative-times (exp p (ord m p)) (ord-rem m p))) (times (exp p (ord m p)) (ord-rem m p)) (commutative-times (exp p (ord m p)) (ord-rem m p))))) m (exp-ord p m (prime-to-lt-SO p H1) H)
not-divides-ord-rem : (m : nat) -> (p : nat) -> (X-- : lt O m) -> (X--1 : lt (S O) p) -> Not lzero (divides p (ord-rem m p))
not-divides-ord-rem = λ (m : nat) -> λ (p : nat) -> λ (H : lt O m) -> λ (H1 : lt (S O) p) -> match-And lzero lzero (Not lzero (divides p (ord-rem m p))) (eq lzero nat m (times (exp p (ord m p)) (ord-rem m p))) lzero (λ (X-- : And lzero lzero (Not lzero (divides p (ord-rem m p))) (eq lzero nat m (times (exp p (ord m p)) (ord-rem m p)))) -> Not lzero (divides p (ord-rem m p))) (λ (H2 : Not lzero (divides p (ord-rem m p))) -> λ (H3 : eq lzero nat m (times (exp p (ord m p)) (ord-rem m p))) -> H2) (p-ord-to-exp1 p m (ord m p) (ord-rem m p) H1 H (eq-pair-fst-snd lzero lzero nat nat (p-ord m p)))
ord-ord-rem : (p : nat) -> (q : nat) -> (m : nat) -> (X-- : lt O m) -> (X--1 : prime p) -> (X--2 : prime q) -> (X--3 : lt q p) -> eq lzero nat (ord (ord-rem m p) q) (ord m q)
ord-ord-rem = λ (p : nat) -> λ (q : nat) -> λ (m : nat) -> λ (H : lt O m) -> λ (H1 : prime p) -> λ (H2 : prime q) -> λ (H3 : lt q p) -> eq-ind-r lzero lzero nat (times (exp p (ord m p)) (ord-rem m p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (exp p (ord m p)) (ord-rem m p))) -> eq lzero nat (ord (ord-rem m p) q) (ord x q)) (eq-ind-r lzero lzero nat (plus (ord (exp p (ord m p)) q) (ord (ord-rem m p) q)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (ord (exp p (ord m p)) q) (ord (ord-rem m p) q))) -> eq lzero nat (ord (ord-rem m p) q) x) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (ord (ord-rem m p) q) (plus x (ord (ord-rem m p) q))) (rewrite-l lzero lzero nat (ord (ord-rem m p) q) (λ (X-- : nat) -> eq lzero nat (ord (ord-rem m p) q) X--) (refl lzero nat (ord (ord-rem m p) q)) (plus O (ord (ord-rem m p) q)) (plus-O-n (ord (ord-rem m p) q))) (ord (exp p (ord m p)) q) (not-divides-to-ord-O q (exp p (ord m p)) H2 (not-to-not lzero (divides q (exp p (ord m p))) (eq lzero nat q p) (divides-exp-to-eq q p (ord m p) H2 H1) (lt-to-not-eq q p H3)))) (ord (times (exp p (ord m p)) (ord-rem m p)) q) (ord-times q (exp p (ord m p)) (ord-rem m p) (lt-O-exp p (ord m p) (prime-to-lt-O p H1)) (lt-O-ord-rem p m (prime-to-lt-SO p H1) H) H2)) m (exp-ord p m (prime-to-lt-SO p H1) H)
lt-ord-rem : (n : nat) -> (m : nat) -> (X-- : prime n) -> (X--1 : lt O m) -> (X--2 : divides n m) -> lt (ord-rem m n) m
lt-ord-rem = λ (n : nat) -> λ (m : nat) -> λ (H : prime n) -> λ (H1 : lt O m) -> λ (H2 : divides n m) -> match-Or lzero lzero (lt (ord-rem m n) m) (eq lzero nat (ord-rem m n) m) lzero (λ (X-- : Or lzero lzero (lt (ord-rem m n) m) (eq lzero nat (ord-rem m n) m)) -> lt (ord-rem m n) m) (λ (auto : lt (ord-rem m n) m) -> auto) (λ (Hm : eq lzero nat (ord-rem m n) m) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt (ord-rem m n) m) (eq-ind lzero lzero nat (ord-rem m n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (ord-rem m n) x-1) -> (X-- : divides n x-1) -> False lzero) (λ (Habs : divides n (ord-rem m n)) -> absurd lzero (divides n (ord-rem m n)) Habs (not-divides-ord-rem m n H1 (prime-to-lt-SO n H))) m Hm H2)) (le-to-or-lt-eq (ord-rem m n) m (divides-to-le (ord-rem m n) m H1 (divides-ord-rem n m (prime-to-lt-SO n H) H1)))
p-ord-inv : (X-p : nat) -> (X-m : nat) -> (X-x : nat) -> nat
p-ord-inv = λ (p : nat) -> λ (m : nat) -> λ (x : nat) -> match-Prod lzero lzero nat nat lzero (λ (X-- : Prod lzero lzero nat nat) -> nat) (λ (q : nat) -> λ (r : nat) -> plus (times r m) q) (p-ord x p)
eq-p-ord-inv : (p : nat) -> (m : nat) -> (x : nat) -> eq lzero nat (p-ord-inv p m x) (plus (times (ord-rem x p) m) (ord x p))
eq-p-ord-inv = λ (p : nat) -> λ (m : nat) -> λ (x : nat) -> match-Prod lzero lzero nat nat lzero (λ (X-- : Prod lzero lzero nat nat) -> eq lzero nat (match-Prod lzero lzero nat nat lzero (λ (X-0 : Prod lzero lzero nat nat) -> nat) (λ (q : nat) -> λ (r : nat) -> plus (times r m) q) X--) (plus (times (snd lzero lzero nat nat X--) m) (fst lzero lzero nat nat X--))) (λ (X-fst : nat) -> λ (X-snd : nat) -> refl lzero nat (match-Prod lzero lzero nat nat lzero (λ (X-- : Prod lzero lzero nat nat) -> nat) (λ (q : nat) -> λ (r : nat) -> plus (times r m) q) (mk-Prod lzero lzero nat nat X-fst X-snd))) (p-ord-aux x x p)
div-p-ord-inv : (p : nat) -> (m : nat) -> (x : nat) -> (X-- : lt (ord x p) m) -> eq lzero nat (div (p-ord-inv p m x) m) (ord-rem x p)
div-p-ord-inv = λ (p : nat) -> λ (m : nat) -> λ (x : nat) -> eq-ind-r lzero lzero nat (plus (times (ord-rem x p) m) (ord x p)) (λ (x0 : nat) -> λ (X-- : eq lzero nat x0 (plus (times (ord-rem x p) m) (ord x p))) -> (X--1 : lt (ord x p) m) -> eq lzero nat (div x0 m) (ord-rem x p)) (div-plus-times m (ord-rem x p) (ord x p)) (p-ord-inv p m x) (eq-p-ord-inv p m x)
mod-p-ord-inv : (p : nat) -> (m : nat) -> (x : nat) -> (X-- : lt (ord x p) m) -> eq lzero nat (mod (p-ord-inv p m x) m) (ord x p)
mod-p-ord-inv = λ (p : nat) -> λ (m : nat) -> λ (x : nat) -> eq-ind-r lzero lzero nat (plus (times (ord-rem x p) m) (ord x p)) (λ (x0 : nat) -> λ (X-- : eq lzero nat x0 (plus (times (ord-rem x p) m) (ord x p))) -> (X--1 : lt (ord x p) m) -> eq lzero nat (mod x0 m) (ord x p)) (mod-plus-times m (ord-rem x p) (ord x p)) (p-ord-inv p m x) (eq-p-ord-inv p m x)