-
Notifications
You must be signed in to change notification settings - Fork 0
/
matita-arithmetics-chinese-reminder.agda
86 lines (60 loc) · 86.5 KB
/
matita-arithmetics-chinese-reminder.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
open import Agda.Primitive
open import matita-arithmetics-minimization
open import matita-basics-bool
open import matita-arithmetics-div-and-mod
open import matita-arithmetics-congruence
open import matita-basics-logic
open import matita-arithmetics-gcd
open import matita-arithmetics-nat
let-clause-1562 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> eq lzero nat (minus (times n c) (times m d)) (S O)
let-clause-1562 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> rewrite-l lzero lzero nat (times d m) (λ (X-- : nat) -> eq lzero nat (minus (times n c) X--) (S O)) (rewrite-l lzero lzero nat (times c n) (λ (X-- : nat) -> eq lzero nat (minus X-- (times d m)) (S O)) H (times n c) (commutative-times c n)) (times m d) (commutative-times d m)
let-clause-1600 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> eq lzero nat (gcd m n) (minus (times n c) (times m d))
let-clause-1600 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (gcd m n) X--) (rewrite-l lzero lzero nat (gcd n m) (λ (X-- : nat) -> eq lzero nat X-- (S O)) pnm (gcd m n) (commutative-gcd n m)) (minus (times n c) (times m d)) (let-clause-1562 m n a b posn posm pnm c X-clearme d X-clearme0 H)
let-clause-15621 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> eq lzero nat (minus (times n c) (times m d)) (S O)
let-clause-15621 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> rewrite-l lzero lzero nat (times d m) (λ (X-- : nat) -> eq lzero nat (minus (times n c) X--) (S O)) (rewrite-l lzero lzero nat (times c n) (λ (X-- : nat) -> eq lzero nat (minus X-- (times d m)) (S O)) H (times n c) (commutative-times c n)) (times m d) (commutative-times d m)
let-clause-16001 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> eq lzero nat (gcd m n) (minus (times n c) (times m d))
let-clause-16001 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (gcd m n) X--) (rewrite-l lzero lzero nat (gcd n m) (λ (X-- : nat) -> eq lzero nat X-- (S O)) pnm (gcd m n) (commutative-gcd n m)) (minus (times n c) (times m d)) (let-clause-15621 m n a b posn posm pnm c X-clearme d X-clearme0 H)
let-clause-1569 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> eq lzero nat (minus (times n c) (times m d)) (S O)
let-clause-1569 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> rewrite-l lzero lzero nat (times d m) (λ (X-- : nat) -> eq lzero nat (minus (times n c) X--) (S O)) (rewrite-l lzero lzero nat (times c n) (λ (X-- : nat) -> eq lzero nat (minus X-- (times d m)) (S O)) H (times n c) (commutative-times c n)) (times m d) (commutative-times d m)
let-clause-15691 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> eq lzero nat (minus (times n c) (times m d)) (S O)
let-clause-15691 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> rewrite-l lzero lzero nat (times d m) (λ (X-- : nat) -> eq lzero nat (minus (times n c) X--) (S O)) (rewrite-l lzero lzero nat (times c n) (λ (X-- : nat) -> eq lzero nat (minus X-- (times d m)) (S O)) H (times n c) (commutative-times c n)) (times m d) (commutative-times d m)
let-clause-1575 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> (x1029 : nat) -> eq lzero nat x1029 (times x1029 (minus (times n c) (times m d)))
let-clause-1575 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> λ (x1029 : nat) -> rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat x1029 (times x1029 X--)) (times-n-1 x1029) (minus (times n c) (times m d)) (let-clause-15691 m n a b posn posm pnm c X-clearme d X-clearme0 H)
let-clause-15692 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> eq lzero nat (minus (times m d) (times n c)) (S O)
let-clause-15692 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> rewrite-l lzero lzero nat (times c n) (λ (X-- : nat) -> eq lzero nat (minus (times m d) X--) (S O)) (rewrite-l lzero lzero nat (times d m) (λ (X-- : nat) -> eq lzero nat (minus X-- (times c n)) (S O)) H (times m d) (commutative-times d m)) (times n c) (commutative-times c n)
let-clause-1607 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> eq lzero nat (gcd m n) (minus (times m d) (times n c))
let-clause-1607 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (gcd m n) X--) (rewrite-l lzero lzero nat (gcd n m) (λ (X-- : nat) -> eq lzero nat X-- (S O)) pnm (gcd m n) (commutative-gcd n m)) (minus (times m d) (times n c)) (let-clause-15692 m n a b posn posm pnm c X-clearme d X-clearme0 H)
let-clause-15622 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> eq lzero nat (minus (times m d) (times n c)) (S O)
let-clause-15622 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> rewrite-l lzero lzero nat (times c n) (λ (X-- : nat) -> eq lzero nat (minus (times m d) X--) (S O)) (rewrite-l lzero lzero nat (times d m) (λ (X-- : nat) -> eq lzero nat (minus X-- (times c n)) (S O)) H (times m d) (commutative-times d m)) (times n c) (commutative-times c n)
let-clause-16002 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> eq lzero nat (gcd m n) (minus (times m d) (times n c))
let-clause-16002 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (gcd m n) X--) (rewrite-l lzero lzero nat (gcd n m) (λ (X-- : nat) -> eq lzero nat X-- (S O)) pnm (gcd m n) (commutative-gcd n m)) (minus (times m d) (times n c)) (let-clause-15622 m n a b posn posm pnm c X-clearme d X-clearme0 H)
let-clause-15623 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> eq lzero nat (minus (times m d) (times n c)) (S O)
let-clause-15623 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> rewrite-l lzero lzero nat (times c n) (λ (X-- : nat) -> eq lzero nat (minus (times m d) X--) (S O)) (rewrite-l lzero lzero nat (times d m) (λ (X-- : nat) -> eq lzero nat (minus X-- (times c n)) (S O)) H (times m d) (commutative-times d m)) (times n c) (commutative-times c n)
let-clause-16003 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> eq lzero nat (gcd m n) (minus (times m d) (times n c))
let-clause-16003 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (gcd m n) X--) (rewrite-l lzero lzero nat (gcd n m) (λ (X-- : nat) -> eq lzero nat X-- (S O)) pnm (gcd m n) (commutative-gcd n m)) (minus (times m d) (times n c)) (let-clause-15623 m n a b posn posm pnm c X-clearme d X-clearme0 H)
let-clause-15624 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> eq lzero nat (minus (times m d) (times n c)) (S O)
let-clause-15624 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> rewrite-l lzero lzero nat (times c n) (λ (X-- : nat) -> eq lzero nat (minus (times m d) X--) (S O)) (rewrite-l lzero lzero nat (times d m) (λ (X-- : nat) -> eq lzero nat (minus X-- (times c n)) (S O)) H (times m d) (commutative-times d m)) (times n c) (commutative-times c n)
let-clause-16004 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> eq lzero nat (gcd m n) (minus (times m d) (times n c))
let-clause-16004 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (gcd m n) X--) (rewrite-l lzero lzero nat (gcd n m) (λ (X-- : nat) -> eq lzero nat X-- (S O)) pnm (gcd m n) (commutative-gcd n m)) (minus (times m d) (times n c)) (let-clause-15624 m n a b posn posm pnm c X-clearme d X-clearme0 H)
let-clause-15625 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> eq lzero nat (minus (times m d) (times n c)) (S O)
let-clause-15625 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> rewrite-l lzero lzero nat (times c n) (λ (X-- : nat) -> eq lzero nat (minus (times m d) X--) (S O)) (rewrite-l lzero lzero nat (times d m) (λ (X-- : nat) -> eq lzero nat (minus X-- (times c n)) (S O)) H (times m d) (commutative-times d m)) (times n c) (commutative-times c n)
let-clause-16005 : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (posn : lt O n) -> (posm : lt O m) -> (pnm : eq lzero nat (gcd n m) (S O)) -> (c : nat) -> (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> (d : nat) -> (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> eq lzero nat (gcd m n) (minus (times m d) (times n c))
let-clause-16005 = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> λ (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat (gcd m n) X--) (rewrite-l lzero lzero nat (gcd n m) (λ (X-- : nat) -> eq lzero nat X-- (S O)) pnm (gcd m n) (commutative-gcd n m)) (minus (times m d) (times n c)) (let-clause-15625 m n a b posn posm pnm c X-clearme d X-clearme0 H)
congruent-ab : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (X-- : lt O n) -> (X--1 : lt O m) -> (X--2 : eq lzero nat (gcd n m) (S O)) -> ex lzero lzero nat (λ (x : nat) -> And lzero lzero (congruent x a m) (congruent x b n))
congruent-ab = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> match-ex lzero lzero nat (λ (c : nat) -> ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) lzero (λ (X-- : ex lzero lzero nat (λ (c : nat) -> ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))))) -> ex lzero lzero nat (λ (x : nat) -> And lzero lzero (congruent x a m) (congruent x b n))) (λ (c : nat) -> λ (X-clearme : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> match-ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) lzero (λ (X-- : ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)))) -> ex lzero lzero nat (λ (x0 : nat) -> And lzero lzero (congruent x0 a m) (congruent x0 b n))) (λ (d : nat) -> λ (X-clearme0 : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> match-Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O)) lzero (λ (X-- : Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) (S O)) (eq lzero nat (minus (times d m) (times c n)) (S O))) -> ex lzero lzero nat (λ (x0 : nat) -> And lzero lzero (congruent x0 a m) (congruent x0 b n))) (λ (H : eq lzero nat (minus (times c n) (times d m)) (S O)) -> ex-intro lzero lzero nat (λ (x0 : nat) -> And lzero lzero (congruent x0 a m) (congruent x0 b n)) (minus (times (times (plus a (times b m)) c) n) (times (times b d) m)) (conj lzero lzero (congruent (minus (times (times (plus a (times b m)) c) n) (times (times b d) m)) a m) (congruent (minus (times (times (plus a (times b m)) c) n) (times (times b d) m)) b n) (eq-ind-r lzero lzero nat (times (plus a (times b m)) (times c n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (plus a (times b m)) (times c n))) -> congruent (minus x (times (times b d) m)) a m) (eq-ind-r lzero lzero nat (plus (times d m) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times d m) (S O))) -> congruent (minus (times (plus a (times b m)) x) (times (times b d) m)) a m) (eq-ind lzero lzero nat (plus (S O) (times d m)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (S O) (times d m)) x-1) -> congruent (minus (times (plus a (times b m)) x-1) (times (times b d) m)) a m) (eq-ind-r lzero lzero nat (plus (times (plus a (times b m)) (S O)) (times (plus a (times b m)) (times d m))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (plus a (times b m)) (S O)) (times (plus a (times b m)) (times d m)))) -> congruent (minus x (times (times b d) m)) a m) (eq-ind lzero lzero nat (plus a (times b m)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus a (times b m)) x-1) -> congruent (minus (plus x-1 (times (plus a (times b m)) (times d m))) (times (times b d) m)) a m) (eq-ind-r lzero lzero nat (plus a (plus (times b m) (times (plus a (times b m)) (times d m)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus a (plus (times b m) (times (plus a (times b m)) (times d m))))) -> congruent (minus x (times (times b d) m)) a m) (eq-ind lzero lzero nat (times (times (plus a (times b m)) d) m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (plus a (times b m)) d) m) x-1) -> congruent (minus (plus a (plus (times b m) x-1)) (times (times b d) m)) a m) (eq-ind lzero lzero nat (times (plus b (times (plus a (times b m)) d)) m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (plus b (times (plus a (times b m)) d)) m) x-1) -> congruent (minus (plus a x-1) (times (times b d) m)) a m) (eq-ind lzero lzero nat (plus (times (plus b (times (plus a (times b m)) d)) m) a) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (times (plus b (times (plus a (times b m)) d)) m) a) x-1) -> congruent (minus x-1 (times (times b d) m)) a m) (eq-ind lzero lzero nat (plus (minus (times (plus b (times (plus a (times b m)) d)) m) (times (times b d) m)) a) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (minus (times (plus b (times (plus a (times b m)) d)) m) (times (times b d) m)) a) x-1) -> congruent x-1 a m) (eq-times-plus-to-congruent (plus (minus (times (plus b (times (plus a (times b m)) d)) m) (times (times b d) m)) a) a m (minus (plus b (times d (plus a (times m b)))) (times b d)) posm (rewrite-r lzero lzero nat (times m b) (λ (X-- : nat) -> eq lzero nat (plus (minus (times (plus b (times (plus a X--) d)) m) (times (times b d) m)) a) (plus (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m) a)) (rewrite-r lzero lzero nat (times d (plus a (times m b))) (λ (X-- : nat) -> eq lzero nat (plus (minus (times (plus b X--) m) (times (times b d) m)) a) (plus (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m) a)) (rewrite-r lzero lzero nat (times m (plus b (times d (plus a (times m b))))) (λ (X-- : nat) -> eq lzero nat (plus (minus X-- (times (times b d) m)) a) (plus (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m) a)) (rewrite-r lzero lzero nat (times m (times b d)) (λ (X-- : nat) -> eq lzero nat (plus (minus (times m (plus b (times d (plus a (times m b))))) X--) a) (plus (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m) a)) (rewrite-l lzero lzero nat (times m (minus (plus b (times d (plus a (times m b)))) (times b d))) (λ (X-- : nat) -> eq lzero nat (plus X-- a) (plus (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m) a)) (rewrite-r lzero lzero nat (plus a (times m (minus (plus b (times d (plus a (times m b)))) (times b d)))) (λ (X-- : nat) -> eq lzero nat X-- (plus (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m) a)) (rewrite-r lzero lzero nat (plus a (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m)) (λ (X-- : nat) -> eq lzero nat (plus a (times m (minus (plus b (times d (plus a (times m b)))) (times b d)))) X--) (rewrite-r lzero lzero nat (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m) (λ (X-- : nat) -> eq lzero nat (plus a X--) (plus a (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m))) (refl lzero nat (plus a (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m))) (times m (minus (plus b (times d (plus a (times m b)))) (times b d))) (commutative-times m (minus (plus b (times d (plus a (times m b)))) (times b d)))) (plus (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m) a) (commutative-plus (times (minus (plus b (times d (plus a (times m b)))) (times b d)) m) a)) (plus (times m (minus (plus b (times d (plus a (times m b)))) (times b d))) a) (commutative-plus (times m (minus (plus b (times d (plus a (times m b)))) (times b d))) a)) (minus (times m (plus b (times d (plus a (times m b))))) (times m (times b d))) (distributive-times-minus m (plus b (times d (plus a (times m b)))) (times b d))) (times (times b d) m) (commutative-times (times b d) m)) (times (plus b (times d (plus a (times m b)))) m) (commutative-times (plus b (times d (plus a (times m b)))) m)) (times (plus a (times m b)) d) (commutative-times (plus a (times m b)) d)) (times b m) (commutative-times b m))) (minus (plus (times (plus b (times (plus a (times b m)) d)) m) a) (times (times b d) m)) (plus-minus (times (times b d) m) (times (plus b (times (plus a (times b m)) d)) m) a (eq-coerc lzero (le (times m (times b d)) (times m (plus b (times d (plus a (times m b)))))) (le (times (times b d) m) (times (plus b (times (plus a (times b m)) d)) m)) (monotonic-le-times-r m (times b d) (plus b (times d (plus a (times m b)))) (transitive-le (times b d) (times (plus a (times b m)) d) (plus b (times d (plus a (times m b)))) (eq-coerc lzero (le (times d b) (times d (plus a (times b m)))) (le (times b d) (times (plus a (times b m)) d)) (monotonic-le-times-r d b (plus a (times b m)) (transitive-le b (times b m) (plus a (times b m)) (eq-coerc lzero (le (gcd O b) (gcd O (times b m))) (le b (times b m)) (le-gcd-times O b m posm) (rewrite-r lzero (lsuc lzero) nat (times m b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (gcd O b) (gcd O (times b m))) (le b X--)) (rewrite-r lzero (lsuc lzero) nat (times m b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (gcd O b) (gcd O X--)) (le b (times m b))) (rewrite-r lzero (lsuc lzero) nat b (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (gcd O (times m b))) (le b (times m b))) (rewrite-r lzero (lsuc lzero) nat (times m b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le b X--) (le b (times m b))) (refl (lsuc lzero) (Set (lzero)) (le b (times m b))) (gcd O (times m b)) (gcd-O-l (times m b))) (gcd O b) (gcd-O-l b)) (times b m) (commutative-times b m)) (times b m) (commutative-times b m))) (eq-coerc lzero (le (times m b) (plus (times m b) a)) (le (times b m) (plus a (times b m))) (le-plus-n-r a (times m b)) (rewrite-r lzero (lsuc lzero) nat (times m b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m b) (plus (times m b) a)) (le X-- (plus a (times b m)))) (rewrite-r lzero (lsuc lzero) nat (times m b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m b) (plus (times m b) a)) (le (times m b) (plus a X--))) (rewrite-r lzero (lsuc lzero) nat (plus a (times m b)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m b) X--) (le (times m b) (plus a (times m b)))) (refl (lsuc lzero) (Set (lzero)) (le (times m b) (plus a (times m b)))) (plus (times m b) a) (commutative-plus (times m b) a)) (times b m) (commutative-times b m)) (times b m) (commutative-times b m))))) (rewrite-r lzero (lsuc lzero) nat (times m b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times d b) (times d (plus a X--))) (le (times b d) (times (plus a X--) d))) (rewrite-r lzero (lsuc lzero) nat (times d (plus a (times m b))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times d b) (times d (plus a (times m b)))) (le (times b d) X--)) (rewrite-r lzero (lsuc lzero) nat (times b d) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (times d (plus a (times m b)))) (le (times b d) (times d (plus a (times m b))))) (refl (lsuc lzero) (Set (lzero)) (le (times b d) (times d (plus a (times m b))))) (times d b) (commutative-times d b)) (times (plus a (times m b)) d) (commutative-times (plus a (times m b)) d)) (times b m) (commutative-times b m))) (eq-coerc lzero (le (times d (plus a (times m b))) (plus (times d (plus a (times m b))) b)) (le (times (plus a (times b m)) d) (plus b (times d (plus a (times m b))))) (le-plus-n-r b (times d (plus a (times m b)))) (rewrite-r lzero (lsuc lzero) nat (times m b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times d (plus a (times m b))) (plus (times d (plus a (times m b))) b)) (le (times (plus a X--) d) (plus b (times d (plus a (times m b)))))) (rewrite-r lzero (lsuc lzero) nat (times d (plus a (times m b))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times d (plus a (times m b))) (plus (times d (plus a (times m b))) b)) (le X-- (plus b (times d (plus a (times m b)))))) (rewrite-r lzero (lsuc lzero) nat (plus b (times d (plus a (times m b)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times d (plus a (times m b))) X--) (le (times d (plus a (times m b))) (plus b (times d (plus a (times m b)))))) (refl (lsuc lzero) (Set (lzero)) (le (times d (plus a (times m b))) (plus b (times d (plus a (times m b)))))) (plus (times d (plus a (times m b))) b) (commutative-plus (times d (plus a (times m b))) b)) (times (plus a (times m b)) d) (commutative-times (plus a (times m b)) d)) (times b m) (commutative-times b m))))) (rewrite-r lzero (lsuc lzero) nat (times m (times b d)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m (times b d)) (times m (plus b (times d (plus a (times m b)))))) (le X-- (times (plus b (times (plus a (times b m)) d)) m))) (rewrite-r lzero (lsuc lzero) nat (times m b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m (times b d)) (times m (plus b (times d (plus a (times m b)))))) (le (times m (times b d)) (times (plus b (times (plus a X--) d)) m))) (rewrite-r lzero (lsuc lzero) nat (times d (plus a (times m b))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m (times b d)) (times m (plus b (times d (plus a (times m b)))))) (le (times m (times b d)) (times (plus b X--) m))) (rewrite-r lzero (lsuc lzero) nat (times m (plus b (times d (plus a (times m b))))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m (times b d)) (times m (plus b (times d (plus a (times m b)))))) (le (times m (times b d)) X--)) (refl (lsuc lzero) (Set (lzero)) (le (times m (times b d)) (times m (plus b (times d (plus a (times m b))))))) (times (plus b (times d (plus a (times m b)))) m) (commutative-times (plus b (times d (plus a (times m b)))) m)) (times (plus a (times m b)) d) (commutative-times (plus a (times m b)) d)) (times b m) (commutative-times b m)) (times (times b d) m) (commutative-times (times b d) m))))) (plus a (times (plus b (times (plus a (times b m)) d)) m)) (commutative-plus (times (plus b (times (plus a (times b m)) d)) m) a)) (plus (times b m) (times (times (plus a (times b m)) d) m)) (distributive-times-plus-r m b (times (plus a (times b m)) d))) (times (plus a (times b m)) (times d m)) (associative-times (plus a (times b m)) d m)) (plus (plus a (times b m)) (times (plus a (times b m)) (times d m))) (associative-plus a (times b m) (times (plus a (times b m)) (times d m)))) (times (plus a (times b m)) (S O)) (times-n-1 (plus a (times b m)))) (times (plus a (times b m)) (plus (S O) (times d m))) (distributive-times-plus (plus a (times b m)) (S O) (times d m))) (plus (times d m) (S O)) (commutative-plus (S O) (times d m))) (times c n) (minus-to-plus (times c n) (times d m) (S O) (transitive-le (times d m) (S (times d m)) (times c n) (le-n-Sn (times d m)) (lt-minus-to-plus-r O (times c n) (times d m) (eq-coerc lzero (lt O (S O)) (lt O (minus (times c n) (times d m))) (lt-O-S O) (rewrite-r lzero (lsuc lzero) nat (times n c) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O (minus X-- (times d m)))) (rewrite-r lzero (lsuc lzero) nat (times m d) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O (minus (times n c) X--))) (rewrite-l lzero (lsuc lzero) nat (gcd m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O X--)) (rewrite-l lzero (lsuc lzero) nat (gcd m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O X--) (lt O (gcd m n))) (refl (lsuc lzero) (Set (lzero)) (lt O (gcd m n))) (S O) (rewrite-r lzero lzero nat (minus (times n c) (times m d)) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (let-clause-1562 m n a b posn posm pnm c X-clearme d X-clearme0 H) (gcd m n) (let-clause-1600 m n a b posn posm pnm c X-clearme d X-clearme0 H))) (minus (times n c) (times m d)) (let-clause-1600 m n a b posn posm pnm c X-clearme d X-clearme0 H)) (times d m) (commutative-times d m)) (times c n) (commutative-times c n))))) (rewrite-r lzero lzero nat (times n c) (λ (X-- : nat) -> eq lzero nat (minus X-- (times d m)) (S O)) (rewrite-r lzero lzero nat (times m d) (λ (X-- : nat) -> eq lzero nat (minus (times n c) X--) (S O)) (rewrite-l lzero lzero nat (gcd m n) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (rewrite-l lzero lzero nat (gcd m n) (λ (X-- : nat) -> eq lzero nat (gcd m n) X--) (refl lzero nat (gcd m n)) (S O) (rewrite-r lzero lzero nat (minus (times n c) (times m d)) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (let-clause-15621 m n a b posn posm pnm c X-clearme d X-clearme0 H) (gcd m n) (let-clause-16001 m n a b posn posm pnm c X-clearme d X-clearme0 H))) (minus (times n c) (times m d)) (let-clause-16001 m n a b posn posm pnm c X-clearme d X-clearme0 H)) (times d m) (commutative-times d m)) (times c n) (commutative-times c n)))) (times (times (plus a (times b m)) c) n) (associative-times (plus a (times b m)) c n)) (eq-ind-r lzero lzero nat (times b (times d m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times b (times d m))) -> congruent (minus (times (times (plus a (times b m)) c) n) x) b n) (eq-ind-r lzero lzero nat (minus (times c n) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (minus (times c n) (S O))) -> congruent (minus (times (times (plus a (times b m)) c) n) (times b x)) b n) (eq-ind-r lzero lzero nat (minus (times b (times c n)) (times b (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (minus (times b (times c n)) (times b (S O)))) -> congruent (minus (times (times (plus a (times b m)) c) n) x) b n) (eq-ind lzero lzero nat (times (times b c) n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times b c) n) x-1) -> congruent (minus (times (times (plus a (times b m)) c) n) (minus x-1 (times b (S O)))) b n) (eq-ind lzero lzero nat (plus (times b (S O)) (minus (times (times (plus a (times b m)) c) n) (times (times b c) n))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (times b (S O)) (minus (times (times (plus a (times b m)) c) n) (times (times b c) n))) x-1) -> congruent x-1 b n) (eq-times-plus-to-congruent (plus (times b (S O)) (minus (times (times (plus a (times b m)) c) n) (times (times b c) n))) b n (minus (times c (plus a (times m b))) (times b c)) posn (rewrite-l lzero lzero nat (minus (times n c) (times m d)) (λ (X-- : nat) -> eq lzero nat (plus (times b X--) (minus (times (times (plus a (times b m)) c) n) (times (times b c) n))) (plus (times (minus (times c (plus a (times m b))) (times b c)) n) b)) (rewrite-l lzero lzero nat b (λ (X-- : nat) -> eq lzero nat (plus X-- (minus (times (times (plus a (times b m)) c) n) (times (times b c) n))) (plus (times (minus (times c (plus a (times m b))) (times b c)) n) b)) (rewrite-r lzero lzero nat (times m b) (λ (X-- : nat) -> eq lzero nat (plus b (minus (times (times (plus a X--) c) n) (times (times b c) n))) (plus (times (minus (times c (plus a (times m b))) (times b c)) n) b)) (rewrite-r lzero lzero nat (times c (plus a (times m b))) (λ (X-- : nat) -> eq lzero nat (plus b (minus (times X-- n) (times (times b c) n))) (plus (times (minus (times c (plus a (times m b))) (times b c)) n) b)) (rewrite-r lzero lzero nat (times n (times c (plus a (times m b)))) (λ (X-- : nat) -> eq lzero nat (plus b (minus X-- (times (times b c) n))) (plus (times (minus (times c (plus a (times m b))) (times b c)) n) b)) (rewrite-r lzero lzero nat (times n (times b c)) (λ (X-- : nat) -> eq lzero nat (plus b (minus (times n (times c (plus a (times m b)))) X--)) (plus (times (minus (times c (plus a (times m b))) (times b c)) n) b)) (rewrite-l lzero lzero nat (times n (minus (times c (plus a (times m b))) (times b c))) (λ (X-- : nat) -> eq lzero nat (plus b X--) (plus (times (minus (times c (plus a (times m b))) (times b c)) n) b)) (rewrite-r lzero lzero nat (plus b (times (minus (times c (plus a (times m b))) (times b c)) n)) (λ (X-- : nat) -> eq lzero nat (plus b (times n (minus (times c (plus a (times m b))) (times b c)))) X--) (rewrite-r lzero lzero nat (times (minus (times c (plus a (times m b))) (times b c)) n) (λ (X-- : nat) -> eq lzero nat (plus b X--) (plus b (times (minus (times c (plus a (times m b))) (times b c)) n))) (refl lzero nat (plus b (times (minus (times c (plus a (times m b))) (times b c)) n))) (times n (minus (times c (plus a (times m b))) (times b c))) (commutative-times n (minus (times c (plus a (times m b))) (times b c)))) (plus (times (minus (times c (plus a (times m b))) (times b c)) n) b) (commutative-plus (times (minus (times c (plus a (times m b))) (times b c)) n) b)) (minus (times n (times c (plus a (times m b)))) (times n (times b c))) (distributive-times-minus n (times c (plus a (times m b))) (times b c))) (times (times b c) n) (commutative-times (times b c) n)) (times (times c (plus a (times m b))) n) (commutative-times (times c (plus a (times m b))) n)) (times (plus a (times m b)) c) (commutative-times (plus a (times m b)) c)) (times b m) (commutative-times b m)) (times b (minus (times n c) (times m d))) (rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat b (times b X--)) (times-n-1 b) (minus (times n c) (times m d)) (let-clause-1569 m n a b posn posm pnm c X-clearme d X-clearme0 H))) (S O) (let-clause-1569 m n a b posn posm pnm c X-clearme d X-clearme0 H))) (minus (times (times (plus a (times b m)) c) n) (minus (times (times b c) n) (times b (S O)))) (minus-minus (times (times (plus a (times b m)) c) n) (times (times b c) n) (times b (S O)) (eq-coerc lzero (le (times b (minus (times n c) (times m d))) (times b (times n c))) (le (times b (S O)) (times (times b c) n)) (monotonic-le-times-r b (minus (times n c) (times m d)) (times n c) (le-plus-to-minus (times n c) (times m d) (times n c) (le-plus-n-r (times m d) (times n c)))) (rewrite-l lzero (lsuc lzero) nat (minus (times n c) (times m d)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b (minus (times n c) (times m d))) (times b (times n c))) (le (times b X--) (times (times b c) n))) (rewrite-l lzero (lsuc lzero) nat b (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b (minus (times n c) (times m d))) (times b (times n c))) (le X-- (times (times b c) n))) (rewrite-r lzero (lsuc lzero) nat (times n (times b c)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b (minus (times n c) (times m d))) (times b (times n c))) (le b X--)) (rewrite-l lzero (lsuc lzero) nat b (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (times b (times n c))) (le b (times n (times b c)))) (rewrite-r lzero (lsuc lzero) nat (times n (times b c)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le b X--) (le b (times n (times b c)))) (refl (lsuc lzero) (Set (lzero)) (le b (times n (times b c)))) (times b (times n c)) (times-times b n c)) (times b (minus (times n c) (times m d))) (let-clause-1575 m n a b posn posm pnm c X-clearme d X-clearme0 H b)) (times (times b c) n) (commutative-times (times b c) n)) (times b (minus (times n c) (times m d))) (let-clause-1575 m n a b posn posm pnm c X-clearme d X-clearme0 H b)) (S O) (let-clause-15691 m n a b posn posm pnm c X-clearme d X-clearme0 H))) (eq-coerc lzero (le (times n (times b c)) (times n (times c (plus a (times m b))))) (le (times (times b c) n) (times (times (plus a (times b m)) c) n)) (monotonic-le-times-r n (times b c) (times c (plus a (times m b))) (eq-ind-r lzero lzero nat (times c b) (λ (x : nat) -> λ (X-- : eq lzero nat x (times c b)) -> le x (times c (plus a (times m b)))) (monotonic-le-times-r c b (plus a (times m b)) (transitive-le b (times m b) (plus a (times m b)) (eq-coerc lzero (le (gcd O b) (gcd O (times b m))) (le b (times m b)) (le-gcd-times O b m posm) (rewrite-r lzero (lsuc lzero) nat (times m b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (gcd O b) (gcd O X--)) (le b (times m b))) (rewrite-r lzero (lsuc lzero) nat b (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (gcd O (times m b))) (le b (times m b))) (rewrite-r lzero (lsuc lzero) nat (times m b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le b X--) (le b (times m b))) (refl (lsuc lzero) (Set (lzero)) (le b (times m b))) (gcd O (times m b)) (gcd-O-l (times m b))) (gcd O b) (gcd-O-l b)) (times b m) (commutative-times b m))) (eq-coerc lzero (le (times m b) (plus (times m b) a)) (le (times m b) (plus a (times m b))) (le-plus-n-r a (times m b)) (rewrite-r lzero (lsuc lzero) nat (plus a (times m b)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m b) X--) (le (times m b) (plus a (times m b)))) (refl (lsuc lzero) (Set (lzero)) (le (times m b) (plus a (times m b)))) (plus (times m b) a) (commutative-plus (times m b) a))))) (times b c) (commutative-times b c))) (rewrite-r lzero (lsuc lzero) nat (times n (times b c)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n (times b c)) (times n (times c (plus a (times m b))))) (le X-- (times (times (plus a (times b m)) c) n))) (rewrite-r lzero (lsuc lzero) nat (times m b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n (times b c)) (times n (times c (plus a (times m b))))) (le (times n (times b c)) (times (times (plus a X--) c) n))) (rewrite-r lzero (lsuc lzero) nat (times c (plus a (times m b))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n (times b c)) (times n (times c (plus a (times m b))))) (le (times n (times b c)) (times X-- n))) (rewrite-r lzero (lsuc lzero) nat (times n (times c (plus a (times m b)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n (times b c)) (times n (times c (plus a (times m b))))) (le (times n (times b c)) X--)) (refl (lsuc lzero) (Set (lzero)) (le (times n (times b c)) (times n (times c (plus a (times m b)))))) (times (times c (plus a (times m b))) n) (commutative-times (times c (plus a (times m b))) n)) (times (plus a (times m b)) c) (commutative-times (plus a (times m b)) c)) (times b m) (commutative-times b m)) (times (times b c) n) (commutative-times (times b c) n))))) (times b (times c n)) (associative-times b c n)) (times b (minus (times c n) (S O))) (distributive-times-minus b (times c n) (S O))) (times d m) (sym-eq lzero nat (minus (times c n) (S O)) (times d m) (plus-to-minus (times c n) (S O) (times d m) (eq-ind-r lzero lzero nat (plus (times d m) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times d m) (S O))) -> eq lzero nat (times c n) x) (minus-to-plus (times c n) (times d m) (S O) (transitive-le (times d m) (S (times d m)) (times c n) (le-n-Sn (times d m)) (lt-minus-to-plus-r O (times c n) (times d m) (eq-coerc lzero (lt O (S O)) (lt O (minus (times c n) (times d m))) (lt-O-S O) (rewrite-r lzero (lsuc lzero) nat (times n c) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O (minus X-- (times d m)))) (rewrite-r lzero (lsuc lzero) nat (times m d) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O (minus (times n c) X--))) (rewrite-l lzero (lsuc lzero) nat (minus (times n c) (times m d)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O X--) (lt O (minus (times n c) (times m d)))) (refl (lsuc lzero) (Set (lzero)) (lt O (minus (times n c) (times m d)))) (S O) (rewrite-l lzero lzero nat (times d m) (λ (X-- : nat) -> eq lzero nat (minus (times n c) X--) (S O)) (rewrite-l lzero lzero nat (times c n) (λ (X-- : nat) -> eq lzero nat (minus X-- (times d m)) (S O)) H (times n c) (commutative-times c n)) (times m d) (commutative-times d m))) (times d m) (commutative-times d m)) (times c n) (commutative-times c n))))) (rewrite-r lzero lzero nat (times n c) (λ (X-- : nat) -> eq lzero nat (minus X-- (times d m)) (S O)) (rewrite-r lzero lzero nat (times m d) (λ (X-- : nat) -> eq lzero nat (minus (times n c) X--) (S O)) (rewrite-l lzero lzero nat (minus (times n c) (times m d)) (λ (X-- : nat) -> eq lzero nat (minus (times n c) (times m d)) X--) (refl lzero nat (minus (times n c) (times m d))) (S O) (rewrite-l lzero lzero nat (times d m) (λ (X-- : nat) -> eq lzero nat (minus (times n c) X--) (S O)) (rewrite-l lzero lzero nat (times c n) (λ (X-- : nat) -> eq lzero nat (minus X-- (times d m)) (S O)) H (times n c) (commutative-times c n)) (times m d) (commutative-times d m))) (times d m) (commutative-times d m)) (times c n) (commutative-times c n))) (plus (S O) (times d m)) (commutative-plus (S O) (times d m)))))) (times (times b d) m) (associative-times b d m)))) (λ (H : eq lzero nat (minus (times d m) (times c n)) (S O)) -> ex-intro lzero lzero nat (λ (x0 : nat) -> And lzero lzero (congruent x0 a m) (congruent x0 b n)) (minus (times (times (plus b (times a n)) d) m) (times (times a c) n)) (conj lzero lzero (congruent (minus (times (times (plus b (times a n)) d) m) (times (times a c) n)) a m) (congruent (minus (times (times (plus b (times a n)) d) m) (times (times a c) n)) b n) (eq-ind-r lzero lzero nat (times a (times c n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times a (times c n))) -> congruent (minus (times (times (plus b (times a n)) d) m) x) a m) (eq-ind-r lzero lzero nat (minus (times d m) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (minus (times d m) (S O))) -> congruent (minus (times (times (plus b (times a n)) d) m) (times a x)) a m) (eq-ind-r lzero lzero nat (minus (times a (times d m)) (times a (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (minus (times a (times d m)) (times a (S O)))) -> congruent (minus (times (times (plus b (times a n)) d) m) x) a m) (eq-ind lzero lzero nat (plus (times a (S O)) (minus (times (times (plus b (times a n)) d) m) (times a (times d m)))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (times a (S O)) (minus (times (times (plus b (times a n)) d) m) (times a (times d m)))) x-1) -> congruent x-1 a m) (eq-times-plus-to-congruent (plus (times a (S O)) (minus (times (times (plus b (times a n)) d) m) (times a (times d m)))) a m (minus (times d (plus b (times n a))) (times a d)) posm (rewrite-l lzero lzero nat (gcd m n) (λ (X-- : nat) -> eq lzero nat (plus (times a X--) (minus (times (times (plus b (times a n)) d) m) (times a (times d m)))) (plus (times (minus (times d (plus b (times n a))) (times a d)) m) a)) (rewrite-l lzero lzero nat a (λ (X-- : nat) -> eq lzero nat (plus X-- (minus (times (times (plus b (times a n)) d) m) (times a (times d m)))) (plus (times (minus (times d (plus b (times n a))) (times a d)) m) a)) (rewrite-r lzero lzero nat (times n a) (λ (X-- : nat) -> eq lzero nat (plus a (minus (times (times (plus b X--) d) m) (times a (times d m)))) (plus (times (minus (times d (plus b (times n a))) (times a d)) m) a)) (rewrite-r lzero lzero nat (times d (plus b (times n a))) (λ (X-- : nat) -> eq lzero nat (plus a (minus (times X-- m) (times a (times d m)))) (plus (times (minus (times d (plus b (times n a))) (times a d)) m) a)) (rewrite-r lzero lzero nat (times m (times d (plus b (times n a)))) (λ (X-- : nat) -> eq lzero nat (plus a (minus X-- (times a (times d m)))) (plus (times (minus (times d (plus b (times n a))) (times a d)) m) a)) (rewrite-r lzero lzero nat (times m d) (λ (X-- : nat) -> eq lzero nat (plus a (minus (times m (times d (plus b (times n a)))) (times a X--))) (plus (times (minus (times d (plus b (times n a))) (times a d)) m) a)) (rewrite-r lzero lzero nat (times m (times a d)) (λ (X-- : nat) -> eq lzero nat (plus a (minus (times m (times d (plus b (times n a)))) X--)) (plus (times (minus (times d (plus b (times n a))) (times a d)) m) a)) (rewrite-l lzero lzero nat (times m (minus (times d (plus b (times n a))) (times a d))) (λ (X-- : nat) -> eq lzero nat (plus a X--) (plus (times (minus (times d (plus b (times n a))) (times a d)) m) a)) (rewrite-r lzero lzero nat (plus a (times (minus (times d (plus b (times n a))) (times a d)) m)) (λ (X-- : nat) -> eq lzero nat (plus a (times m (minus (times d (plus b (times n a))) (times a d)))) X--) (rewrite-r lzero lzero nat (times (minus (times d (plus b (times n a))) (times a d)) m) (λ (X-- : nat) -> eq lzero nat (plus a X--) (plus a (times (minus (times d (plus b (times n a))) (times a d)) m))) (refl lzero nat (plus a (times (minus (times d (plus b (times n a))) (times a d)) m))) (times m (minus (times d (plus b (times n a))) (times a d))) (commutative-times m (minus (times d (plus b (times n a))) (times a d)))) (plus (times (minus (times d (plus b (times n a))) (times a d)) m) a) (commutative-plus (times (minus (times d (plus b (times n a))) (times a d)) m) a)) (minus (times m (times d (plus b (times n a)))) (times m (times a d))) (distributive-times-minus m (times d (plus b (times n a))) (times a d))) (times a (times m d)) (times-times a m d)) (times d m) (commutative-times d m)) (times (times d (plus b (times n a))) m) (commutative-times (times d (plus b (times n a))) m)) (times (plus b (times n a)) d) (commutative-times (plus b (times n a)) d)) (times a n) (commutative-times a n)) (times a (gcd m n)) (rewrite-r lzero lzero nat (minus (times m d) (times n c)) (λ (X-- : nat) -> eq lzero nat a (times a X--)) (rewrite-r lzero lzero nat (S O) (λ (X-- : nat) -> eq lzero nat a (times a X--)) (times-n-1 a) (minus (times m d) (times n c)) (let-clause-15692 m n a b posn posm pnm c X-clearme d X-clearme0 H)) (gcd m n) (let-clause-1607 m n a b posn posm pnm c X-clearme d X-clearme0 H))) (S O) (rewrite-r lzero lzero nat (minus (times m d) (times n c)) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (let-clause-15692 m n a b posn posm pnm c X-clearme d X-clearme0 H) (gcd m n) (let-clause-1607 m n a b posn posm pnm c X-clearme d X-clearme0 H)))) (minus (times (times (plus b (times a n)) d) m) (minus (times a (times d m)) (times a (S O)))) (minus-minus (times (times (plus b (times a n)) d) m) (times a (times d m)) (times a (S O)) (monotonic-le-times-r a (S O) (times d m) (eq-ind lzero lzero nat (minus (times d m) (times c n)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (minus (times d m) (times c n)) x-1) -> le x-1 (times d m)) (le-plus-to-minus (times d m) (times c n) (times d m) (le-plus-n-r (times c n) (times d m))) (S O) H)) (eq-ind lzero lzero nat (times (times a d) m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times a d) m) x-1) -> le x-1 (times (times (plus b (times a n)) d) m)) (eq-coerc lzero (le (times m (times a d)) (times m (times d (plus b (times n a))))) (le (times (times a d) m) (times (times (plus b (times a n)) d) m)) (monotonic-le-times-r m (times a d) (times d (plus b (times n a))) (eq-ind-r lzero lzero nat (times d a) (λ (x : nat) -> λ (X-- : eq lzero nat x (times d a)) -> le x (times d (plus b (times n a)))) (monotonic-le-times-r d a (plus b (times n a)) (transitive-le a (times n a) (plus b (times n a)) (eq-coerc lzero (le (gcd O a) (gcd O (times a n))) (le a (times n a)) (le-gcd-times O a n posn) (rewrite-r lzero (lsuc lzero) nat (times n a) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (gcd O a) (gcd O X--)) (le a (times n a))) (rewrite-r lzero (lsuc lzero) nat a (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (gcd O (times n a))) (le a (times n a))) (rewrite-r lzero (lsuc lzero) nat (times n a) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le a X--) (le a (times n a))) (refl (lsuc lzero) (Set (lzero)) (le a (times n a))) (gcd O (times n a)) (gcd-O-l (times n a))) (gcd O a) (gcd-O-l a)) (times a n) (commutative-times a n))) (eq-coerc lzero (le (times n a) (plus (times n a) b)) (le (times n a) (plus b (times n a))) (le-plus-n-r b (times n a)) (rewrite-r lzero (lsuc lzero) nat (plus b (times n a)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n a) X--) (le (times n a) (plus b (times n a)))) (refl (lsuc lzero) (Set (lzero)) (le (times n a) (plus b (times n a)))) (plus (times n a) b) (commutative-plus (times n a) b))))) (times a d) (commutative-times a d))) (rewrite-r lzero (lsuc lzero) nat (times m (times a d)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m (times a d)) (times m (times d (plus b (times n a))))) (le X-- (times (times (plus b (times a n)) d) m))) (rewrite-r lzero (lsuc lzero) nat (times n a) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m (times a d)) (times m (times d (plus b (times n a))))) (le (times m (times a d)) (times (times (plus b X--) d) m))) (rewrite-r lzero (lsuc lzero) nat (times d (plus b (times n a))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m (times a d)) (times m (times d (plus b (times n a))))) (le (times m (times a d)) (times X-- m))) (rewrite-r lzero (lsuc lzero) nat (times m (times d (plus b (times n a)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times m (times a d)) (times m (times d (plus b (times n a))))) (le (times m (times a d)) X--)) (refl (lsuc lzero) (Set (lzero)) (le (times m (times a d)) (times m (times d (plus b (times n a)))))) (times (times d (plus b (times n a))) m) (commutative-times (times d (plus b (times n a))) m)) (times (plus b (times n a)) d) (commutative-times (plus b (times n a)) d)) (times a n) (commutative-times a n)) (times (times a d) m) (commutative-times (times a d) m))) (times a (times d m)) (associative-times a d m)))) (times a (minus (times d m) (S O))) (distributive-times-minus a (times d m) (S O))) (times c n) (sym-eq lzero nat (minus (times d m) (S O)) (times c n) (plus-to-minus (times d m) (S O) (times c n) (eq-ind-r lzero lzero nat (plus (times c n) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times c n) (S O))) -> eq lzero nat (times d m) x) (minus-to-plus (times d m) (times c n) (S O) (transitive-le (times c n) (S (times c n)) (times d m) (le-n-Sn (times c n)) (lt-minus-to-plus-r O (times d m) (times c n) (eq-coerc lzero (lt O (S O)) (lt O (minus (times d m) (times c n))) (lt-O-S O) (rewrite-r lzero (lsuc lzero) nat (times m d) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O (minus X-- (times c n)))) (rewrite-r lzero (lsuc lzero) nat (times n c) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O (minus (times m d) X--))) (rewrite-l lzero (lsuc lzero) nat (gcd m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O X--)) (rewrite-l lzero (lsuc lzero) nat (gcd m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O X--) (lt O (gcd m n))) (refl (lsuc lzero) (Set (lzero)) (lt O (gcd m n))) (S O) (rewrite-r lzero lzero nat (minus (times m d) (times n c)) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (let-clause-15622 m n a b posn posm pnm c X-clearme d X-clearme0 H) (gcd m n) (let-clause-16002 m n a b posn posm pnm c X-clearme d X-clearme0 H))) (minus (times m d) (times n c)) (let-clause-16002 m n a b posn posm pnm c X-clearme d X-clearme0 H)) (times c n) (commutative-times c n)) (times d m) (commutative-times d m))))) (rewrite-r lzero lzero nat (times m d) (λ (X-- : nat) -> eq lzero nat (minus X-- (times c n)) (S O)) (rewrite-r lzero lzero nat (times n c) (λ (X-- : nat) -> eq lzero nat (minus (times m d) X--) (S O)) (rewrite-l lzero lzero nat (gcd m n) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (rewrite-l lzero lzero nat (gcd m n) (λ (X-- : nat) -> eq lzero nat (gcd m n) X--) (refl lzero nat (gcd m n)) (S O) (rewrite-r lzero lzero nat (minus (times m d) (times n c)) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (let-clause-15623 m n a b posn posm pnm c X-clearme d X-clearme0 H) (gcd m n) (let-clause-16003 m n a b posn posm pnm c X-clearme d X-clearme0 H))) (minus (times m d) (times n c)) (let-clause-16003 m n a b posn posm pnm c X-clearme d X-clearme0 H)) (times c n) (commutative-times c n)) (times d m) (commutative-times d m))) (plus (S O) (times c n)) (commutative-plus (S O) (times c n)))))) (times (times a c) n) (associative-times a c n)) (eq-ind-r lzero lzero nat (times (plus b (times a n)) (times d m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (plus b (times a n)) (times d m))) -> congruent (minus x (times (times a c) n)) b n) (eq-ind-r lzero lzero nat (plus (times c n) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times c n) (S O))) -> congruent (minus (times (plus b (times a n)) x) (times (times a c) n)) b n) (eq-ind-r lzero lzero nat (plus (S O) (times c n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (S O) (times c n))) -> congruent (minus (times (plus b (times a n)) x) (times (times a c) n)) b n) (eq-ind-r lzero lzero nat (plus (times (plus b (times a n)) (S O)) (times (plus b (times a n)) (times c n))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (plus b (times a n)) (S O)) (times (plus b (times a n)) (times c n)))) -> congruent (minus x (times (times a c) n)) b n) (eq-ind lzero lzero nat (plus b (times a n)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus b (times a n)) x-1) -> congruent (minus (plus x-1 (times (plus b (times a n)) (times c n))) (times (times a c) n)) b n) (eq-ind lzero lzero nat (times (times (plus b (times a n)) c) n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (plus b (times a n)) c) n) x-1) -> congruent (minus (plus (plus b (times a n)) x-1) (times (times a c) n)) b n) (eq-ind-r lzero lzero nat (plus b (plus (times a n) (times (times (plus b (times a n)) c) n))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus b (plus (times a n) (times (times (plus b (times a n)) c) n)))) -> congruent (minus x (times (times a c) n)) b n) (eq-ind lzero lzero nat (times (plus a (times (plus b (times a n)) c)) n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (plus a (times (plus b (times a n)) c)) n) x-1) -> congruent (minus (plus b x-1) (times (times a c) n)) b n) (eq-ind lzero lzero nat (plus (times (plus a (times (plus b (times a n)) c)) n) b) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (times (plus a (times (plus b (times a n)) c)) n) b) x-1) -> congruent (minus x-1 (times (times a c) n)) b n) (eq-ind lzero lzero nat (plus (minus (times (plus a (times (plus b (times a n)) c)) n) (times (times a c) n)) b) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (minus (times (plus a (times (plus b (times a n)) c)) n) (times (times a c) n)) b) x-1) -> congruent x-1 b n) (eq-times-plus-to-congruent (plus (minus (times (plus a (times (plus b (times a n)) c)) n) (times (times a c) n)) b) b n (minus (plus a (times c (plus b (times n a)))) (times a c)) posn (rewrite-r lzero lzero nat (times n a) (λ (X-- : nat) -> eq lzero nat (plus (minus (times (plus a (times (plus b X--) c)) n) (times (times a c) n)) b) (plus (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n) b)) (rewrite-r lzero lzero nat (times c (plus b (times n a))) (λ (X-- : nat) -> eq lzero nat (plus (minus (times (plus a X--) n) (times (times a c) n)) b) (plus (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n) b)) (rewrite-r lzero lzero nat (times n (plus a (times c (plus b (times n a))))) (λ (X-- : nat) -> eq lzero nat (plus (minus X-- (times (times a c) n)) b) (plus (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n) b)) (rewrite-r lzero lzero nat (times n (times a c)) (λ (X-- : nat) -> eq lzero nat (plus (minus (times n (plus a (times c (plus b (times n a))))) X--) b) (plus (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n) b)) (rewrite-l lzero lzero nat (times n (minus (plus a (times c (plus b (times n a)))) (times a c))) (λ (X-- : nat) -> eq lzero nat (plus X-- b) (plus (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n) b)) (rewrite-r lzero lzero nat (plus b (times n (minus (plus a (times c (plus b (times n a)))) (times a c)))) (λ (X-- : nat) -> eq lzero nat X-- (plus (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n) b)) (rewrite-r lzero lzero nat (plus b (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n)) (λ (X-- : nat) -> eq lzero nat (plus b (times n (minus (plus a (times c (plus b (times n a)))) (times a c)))) X--) (rewrite-r lzero lzero nat (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n) (λ (X-- : nat) -> eq lzero nat (plus b X--) (plus b (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n))) (refl lzero nat (plus b (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n))) (times n (minus (plus a (times c (plus b (times n a)))) (times a c))) (commutative-times n (minus (plus a (times c (plus b (times n a)))) (times a c)))) (plus (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n) b) (commutative-plus (times (minus (plus a (times c (plus b (times n a)))) (times a c)) n) b)) (plus (times n (minus (plus a (times c (plus b (times n a)))) (times a c))) b) (commutative-plus (times n (minus (plus a (times c (plus b (times n a)))) (times a c))) b)) (minus (times n (plus a (times c (plus b (times n a))))) (times n (times a c))) (distributive-times-minus n (plus a (times c (plus b (times n a)))) (times a c))) (times (times a c) n) (commutative-times (times a c) n)) (times (plus a (times c (plus b (times n a)))) n) (commutative-times (plus a (times c (plus b (times n a)))) n)) (times (plus b (times n a)) c) (commutative-times (plus b (times n a)) c)) (times a n) (commutative-times a n))) (minus (plus (times (plus a (times (plus b (times a n)) c)) n) b) (times (times a c) n)) (plus-minus (times (times a c) n) (times (plus a (times (plus b (times a n)) c)) n) b (eq-coerc lzero (le (times n (times a c)) (times n (plus a (times c (plus b (times n a)))))) (le (times (times a c) n) (times (plus a (times (plus b (times a n)) c)) n)) (monotonic-le-times-r n (times a c) (plus a (times c (plus b (times n a)))) (transitive-le (times a c) (times c (plus b (times n a))) (plus a (times c (plus b (times n a)))) (eq-ind lzero lzero nat (times c a) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times c a) x-1) -> le x-1 (times c (plus b (times n a)))) (monotonic-le-times-r c a (plus b (times n a)) (transitive-le a (times n a) (plus b (times n a)) (eq-coerc lzero (le (gcd O a) (gcd O (times a n))) (le a (times n a)) (le-gcd-times O a n posn) (rewrite-r lzero (lsuc lzero) nat (times n a) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (gcd O a) (gcd O X--)) (le a (times n a))) (rewrite-r lzero (lsuc lzero) nat a (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (gcd O (times n a))) (le a (times n a))) (rewrite-r lzero (lsuc lzero) nat (times n a) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le a X--) (le a (times n a))) (refl (lsuc lzero) (Set (lzero)) (le a (times n a))) (gcd O (times n a)) (gcd-O-l (times n a))) (gcd O a) (gcd-O-l a)) (times a n) (commutative-times a n))) (eq-coerc lzero (le (times n a) (plus (times n a) b)) (le (times n a) (plus b (times n a))) (le-plus-n-r b (times n a)) (rewrite-r lzero (lsuc lzero) nat (plus b (times n a)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n a) X--) (le (times n a) (plus b (times n a)))) (refl (lsuc lzero) (Set (lzero)) (le (times n a) (plus b (times n a)))) (plus (times n a) b) (commutative-plus (times n a) b))))) (times a c) (commutative-times c a)) (eq-coerc lzero (le (times c (plus b (times n a))) (plus (times c (plus b (times n a))) a)) (le (times c (plus b (times n a))) (plus a (times c (plus b (times n a))))) (le-plus-n-r a (times c (plus b (times n a)))) (rewrite-r lzero (lsuc lzero) nat (plus a (times c (plus b (times n a)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times c (plus b (times n a))) X--) (le (times c (plus b (times n a))) (plus a (times c (plus b (times n a)))))) (refl (lsuc lzero) (Set (lzero)) (le (times c (plus b (times n a))) (plus a (times c (plus b (times n a)))))) (plus (times c (plus b (times n a))) a) (commutative-plus (times c (plus b (times n a))) a))))) (rewrite-r lzero (lsuc lzero) nat (times n (times a c)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n (times a c)) (times n (plus a (times c (plus b (times n a)))))) (le X-- (times (plus a (times (plus b (times a n)) c)) n))) (rewrite-r lzero (lsuc lzero) nat (times n a) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n (times a c)) (times n (plus a (times c (plus b (times n a)))))) (le (times n (times a c)) (times (plus a (times (plus b X--) c)) n))) (rewrite-r lzero (lsuc lzero) nat (times c (plus b (times n a))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n (times a c)) (times n (plus a (times c (plus b (times n a)))))) (le (times n (times a c)) (times (plus a X--) n))) (rewrite-r lzero (lsuc lzero) nat (times n (plus a (times c (plus b (times n a))))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n (times a c)) (times n (plus a (times c (plus b (times n a)))))) (le (times n (times a c)) X--)) (refl (lsuc lzero) (Set (lzero)) (le (times n (times a c)) (times n (plus a (times c (plus b (times n a))))))) (times (plus a (times c (plus b (times n a)))) n) (commutative-times (plus a (times c (plus b (times n a)))) n)) (times (plus b (times n a)) c) (commutative-times (plus b (times n a)) c)) (times a n) (commutative-times a n)) (times (times a c) n) (commutative-times (times a c) n))))) (plus b (times (plus a (times (plus b (times a n)) c)) n)) (commutative-plus (times (plus a (times (plus b (times a n)) c)) n) b)) (plus (times a n) (times (times (plus b (times a n)) c) n)) (distributive-times-plus-r n a (times (plus b (times a n)) c))) (plus (plus b (times a n)) (times (times (plus b (times a n)) c) n)) (associative-plus b (times a n) (times (times (plus b (times a n)) c) n))) (times (plus b (times a n)) (times c n)) (associative-times (plus b (times a n)) c n)) (times (plus b (times a n)) (S O)) (times-n-1 (plus b (times a n)))) (times (plus b (times a n)) (plus (S O) (times c n))) (distributive-times-plus (plus b (times a n)) (S O) (times c n))) (plus (times c n) (S O)) (commutative-plus (times c n) (S O))) (times d m) (minus-to-plus (times d m) (times c n) (S O) (transitive-le (times c n) (S (times c n)) (times d m) (le-n-Sn (times c n)) (lt-minus-to-plus-r O (times d m) (times c n) (eq-coerc lzero (lt O (S O)) (lt O (minus (times d m) (times c n))) (lt-O-S O) (rewrite-r lzero (lsuc lzero) nat (times m d) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O (minus X-- (times c n)))) (rewrite-r lzero (lsuc lzero) nat (times n c) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O (minus (times m d) X--))) (rewrite-l lzero (lsuc lzero) nat (gcd m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O (S O)) (lt O X--)) (rewrite-l lzero (lsuc lzero) nat (gcd m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O X--) (lt O (gcd m n))) (refl (lsuc lzero) (Set (lzero)) (lt O (gcd m n))) (S O) (rewrite-r lzero lzero nat (minus (times m d) (times n c)) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (let-clause-15624 m n a b posn posm pnm c X-clearme d X-clearme0 H) (gcd m n) (let-clause-16004 m n a b posn posm pnm c X-clearme d X-clearme0 H))) (minus (times m d) (times n c)) (let-clause-16004 m n a b posn posm pnm c X-clearme d X-clearme0 H)) (times c n) (commutative-times c n)) (times d m) (commutative-times d m))))) (rewrite-r lzero lzero nat (times m d) (λ (X-- : nat) -> eq lzero nat (minus X-- (times c n)) (S O)) (rewrite-r lzero lzero nat (times n c) (λ (X-- : nat) -> eq lzero nat (minus (times m d) X--) (S O)) (rewrite-l lzero lzero nat (gcd m n) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (rewrite-l lzero lzero nat (gcd m n) (λ (X-- : nat) -> eq lzero nat (gcd m n) X--) (refl lzero nat (gcd m n)) (S O) (rewrite-r lzero lzero nat (minus (times m d) (times n c)) (λ (X-- : nat) -> eq lzero nat X-- (S O)) (let-clause-15625 m n a b posn posm pnm c X-clearme d X-clearme0 H) (gcd m n) (let-clause-16005 m n a b posn posm pnm c X-clearme d X-clearme0 H))) (minus (times m d) (times n c)) (let-clause-16005 m n a b posn posm pnm c X-clearme d X-clearme0 H)) (times c n) (commutative-times c n)) (times d m) (commutative-times d m)))) (times (times (plus b (times a n)) d) m) (associative-times (plus b (times a n)) d m)))) X-clearme0) X-clearme) (eq-ind lzero lzero nat (gcd n m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (gcd n m) x-1) -> ex lzero lzero nat (λ (c : nat) -> ex lzero lzero nat (λ (d : nat) -> Or lzero lzero (eq lzero nat (minus (times c n) (times d m)) x-1) (eq lzero nat (minus (times d m) (times c n)) x-1)))) (eq-minus-gcd m n) (S O) pnm)
congruent-ab-lt : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (X-- : lt O n) -> (X--1 : lt O m) -> (X--2 : eq lzero nat (gcd n m) (S O)) -> ex lzero lzero nat (λ (x : nat) -> And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n)))
congruent-ab-lt = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> match-ex lzero lzero nat (λ (x : nat) -> And lzero lzero (congruent x a m) (congruent x b n)) lzero (λ (X-- : ex lzero lzero nat (λ (x : nat) -> And lzero lzero (congruent x a m) (congruent x b n))) -> ex lzero lzero nat (λ (x : nat) -> And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n)))) (λ (x : nat) -> λ (X-clearme : And lzero lzero (congruent x a m) (congruent x b n)) -> match-And lzero lzero (congruent x a m) (congruent x b n) lzero (λ (X-- : And lzero lzero (congruent x a m) (congruent x b n)) -> ex lzero lzero nat (λ (x0 : nat) -> And lzero lzero (And lzero lzero (congruent x0 a m) (congruent x0 b n)) (lt x0 (times m n)))) (λ (cxa : congruent x a m) -> λ (cxb : congruent x b n) -> ex-intro lzero lzero nat (λ (x0 : nat) -> And lzero lzero (And lzero lzero (congruent x0 a m) (congruent x0 b n)) (lt x0 (times m n))) (mod x (times m n)) (conj lzero lzero (And lzero lzero (congruent (mod x (times m n)) a m) (congruent (mod x (times m n)) b n)) (lt (mod x (times m n)) (times m n)) (conj lzero lzero (congruent (mod x (times m n)) a m) (congruent (mod x (times m n)) b n) (transitive-congruent m (mod x (times m n)) x a (sym-eq lzero nat (mod x m) (mod (mod x (times m n)) m) (eq-ind-r lzero lzero nat (times n m) (λ (x0 : nat) -> λ (X-- : eq lzero nat x0 (times n m)) -> eq lzero nat (mod x m) (mod (mod x x0) m)) (congruent-n-mod-times x n m posm posn) (times m n) (commutative-times m n))) cxa) (transitive-congruent n (mod x (times m n)) x b (sym-eq lzero nat (mod x n) (mod (mod x (times m n)) n) (congruent-n-mod-times x m n posn posm)) cxb)) (lt-mod-m-m x (times m n) (eq-ind-r lzero lzero nat (times O O) (λ (x0 : nat) -> λ (X-- : eq lzero nat x0 (times O O)) -> lt x0 (times m n)) (lt-times O m O n posm posn) O (times-n-O O))))) X-clearme) (congruent-ab m n a b posn posm pnm)
cr-pair : (X-n : nat) -> (X-m : nat) -> (X-a : nat) -> (X-b : nat) -> nat
cr-pair = λ (n : nat) -> λ (m : nat) -> λ (a : nat) -> λ (b : nat) -> min' (times n m) O (λ (x : nat) -> andb (eqb (mod x n) a) (eqb (mod x m) b))
cr-pair1 : eq lzero nat (cr-pair (S (S O)) (S (S (S O))) O O) O
cr-pair1 = refl lzero nat (cr-pair (S (S O)) (S (S (S O))) O O)
cr-pair2 : eq lzero nat (cr-pair (S (S O)) (S (S (S O))) (S O) O) (S (S (S O)))
cr-pair2 = refl lzero nat (cr-pair (S (S O)) (S (S (S O))) (S O) O)
cr-pair3 : eq lzero nat (cr-pair (S (S O)) (S (S (S O))) (S O) (S (S O))) (S (S (S (S (S O)))))
cr-pair3 = refl lzero nat (cr-pair (S (S O)) (S (S (S O))) (S O) (S (S O)))
cr-pair4 : eq lzero nat (cr-pair (S (S (S (S (S O))))) (S (S (S (S (S (S (S O))))))) (S (S (S O))) (S (S O))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))
cr-pair4 = refl lzero nat (cr-pair (S (S (S (S (S O))))) (S (S (S (S (S (S (S O))))))) (S (S (S O))) (S (S O)))
cr-pair5 : eq lzero nat (cr-pair (S (S (S O))) (S (S (S (S (S (S (S O))))))) O (S (S (S (S O))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))
cr-pair5 = refl lzero nat (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))
mod-cr-pair : (m : nat) -> (n : nat) -> (a : nat) -> (b : nat) -> (X-- : lt a m) -> (X--1 : lt b n) -> (X--2 : eq lzero nat (gcd n m) (S O)) -> And lzero lzero (eq lzero nat (mod (cr-pair m n a b) m) a) (eq lzero nat (mod (cr-pair m n a b) n) b)
mod-cr-pair = λ (m : nat) -> λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> λ (ltam : lt a m) -> λ (ltbn : lt b n) -> λ (pnm : eq lzero nat (gcd n m) (S O)) -> eq-ind-r lzero lzero nat a (λ (x : nat) -> λ (X-- : eq lzero nat x a) -> And lzero lzero (eq lzero nat x a) (eq lzero nat (mod (cr-pair m n a b) n) b)) (eq-ind-r lzero lzero nat b (λ (x : nat) -> λ (X-- : eq lzero nat x b) -> And lzero lzero (eq lzero nat a a) (eq lzero nat x b)) (conj lzero lzero (eq lzero nat a a) (eq lzero nat b b) (refl lzero nat a) (refl lzero nat b)) (mod (cr-pair m n a b) n) (eqb-true-to-eq (mod (cr-pair m n a b) n) b (andb-true-r (eqb (mod (cr-pair m n a b) m) a) (eqb (mod (cr-pair m n a b) n) b) (f-min-true (λ (X-- : nat) -> andb (eqb (mod X-- m) a) (eqb (mod X-- n) b)) (times m n) O (match-ex lzero lzero nat (λ (x : nat) -> And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n))) lzero (λ (X-- : ex lzero lzero nat (λ (x : nat) -> And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n)))) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le O i) (lt i (plus (times m n) O))) (eq lzero bool (andb (eqb (mod i m) a) (eqb (mod i n) b)) true))) (λ (x : nat) -> λ (X-clearme : And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n))) -> match-And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n)) lzero (λ (X-- : And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n))) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le O i) (lt i (plus (times m n) O))) (eq lzero bool (andb (eqb (mod i m) a) (eqb (mod i n) b)) true))) (λ (X-clearme0 : And lzero lzero (congruent x a m) (congruent x b n)) -> match-And lzero lzero (congruent x a m) (congruent x b n) lzero (λ (X-- : And lzero lzero (congruent x a m) (congruent x b n)) -> (X--1 : lt x (times m n)) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le O i) (lt i (plus (times m n) O))) (eq lzero bool (andb (eqb (mod i m) a) (eqb (mod i n) b)) true))) (λ (cxa : congruent x a m) -> λ (cxb : congruent x b n) -> λ (ltx : lt x (times m n)) -> ex-intro lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le O i) (lt i (plus (times m n) O))) (eq lzero bool (andb (eqb (mod i m) a) (eqb (mod i n) b)) true)) x (conj lzero lzero (And lzero lzero (le O x) (lt x (plus (times m n) O))) (eq lzero bool (andb (eqb (mod x m) a) (eqb (mod x n) b)) true) (conj lzero lzero (le O x) (lt x (plus (times m n) O)) (le-O-n x) (eq-coerc lzero (le (S x) (times m n)) (le (S x) (plus (times m n) O)) ltx (rewrite-r lzero (lsuc lzero) nat (plus O (times m n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S x) (times m n)) (le (S x) X--)) (rewrite-l lzero (lsuc lzero) nat (times m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S x) (times m n)) (le (S x) X--)) (refl (lsuc lzero) (Set (lzero)) (le (S x) (times m n))) (plus O (times m n)) (plus-O-n (times m n))) (plus (times m n) O) (commutative-plus (times m n) O)))) (eq-ind-r lzero lzero bool true (λ (x0 : bool) -> λ (X-- : eq lzero bool x0 true) -> eq lzero bool (andb x0 (eqb (mod x n) b)) true) (eq-ind-r lzero lzero bool true (λ (x0 : bool) -> λ (X-- : eq lzero bool x0 true) -> eq lzero bool (andb true x0) true) (refl lzero bool (andb true true)) (eqb (mod x n) b) (eq-to-eqb-true (mod x n) b (eq-ind lzero lzero nat (mod b n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (mod b n) x-1) -> eq lzero nat (mod x n) x-1) (rewrite-r lzero lzero nat (mod b n) (λ (X-- : nat) -> eq lzero nat X-- (mod b n)) (refl lzero nat (mod b n)) (mod x n) cxb) b (lt-to-eq-mod b n ltbn)))) (eqb (mod x m) a) (eq-to-eqb-true (mod x m) a (eq-ind lzero lzero nat (mod a m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (mod a m) x-1) -> eq lzero nat (mod x m) x-1) (rewrite-r lzero lzero nat (mod a m) (λ (X-- : nat) -> eq lzero nat X-- (mod a m)) (refl lzero nat (mod a m)) (mod x m) cxa) a (lt-to-eq-mod a m ltam)))))) X-clearme0) X-clearme) (congruent-ab-lt m n a b (le-to-lt-to-lt O b n (le-O-n b) ltbn) (le-to-lt-to-lt O a m (le-O-n a) ltam) pnm)))))) (mod (cr-pair m n a b) m) (eqb-true-to-eq (mod (cr-pair m n a b) m) a (andb-true-l (eqb (mod (cr-pair m n a b) m) a) (eqb (mod (cr-pair m n a b) n) b) (f-min-true (λ (X-- : nat) -> andb (eqb (mod X-- m) a) (eqb (mod X-- n) b)) (times m n) O (match-ex lzero lzero nat (λ (x : nat) -> And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n))) lzero (λ (X-- : ex lzero lzero nat (λ (x : nat) -> And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n)))) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le O i) (lt i (plus (times m n) O))) (eq lzero bool (andb (eqb (mod i m) a) (eqb (mod i n) b)) true))) (λ (x : nat) -> λ (X-clearme : And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n))) -> match-And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n)) lzero (λ (X-- : And lzero lzero (And lzero lzero (congruent x a m) (congruent x b n)) (lt x (times m n))) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le O i) (lt i (plus (times m n) O))) (eq lzero bool (andb (eqb (mod i m) a) (eqb (mod i n) b)) true))) (λ (X-clearme0 : And lzero lzero (congruent x a m) (congruent x b n)) -> match-And lzero lzero (congruent x a m) (congruent x b n) lzero (λ (X-- : And lzero lzero (congruent x a m) (congruent x b n)) -> (X--1 : lt x (times m n)) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le O i) (lt i (plus (times m n) O))) (eq lzero bool (andb (eqb (mod i m) a) (eqb (mod i n) b)) true))) (λ (cxa : congruent x a m) -> λ (cxb : congruent x b n) -> λ (ltx : lt x (times m n)) -> ex-intro lzero lzero nat (λ (i : nat) -> And lzero lzero (And lzero lzero (le O i) (lt i (plus (times m n) O))) (eq lzero bool (andb (eqb (mod i m) a) (eqb (mod i n) b)) true)) x (conj lzero lzero (And lzero lzero (le O x) (lt x (plus (times m n) O))) (eq lzero bool (andb (eqb (mod x m) a) (eqb (mod x n) b)) true) (conj lzero lzero (le O x) (lt x (plus (times m n) O)) (le-O-n x) (eq-coerc lzero (le (S x) (times m n)) (le (S x) (plus (times m n) O)) ltx (rewrite-r lzero (lsuc lzero) nat (plus O (times m n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S x) (times m n)) (le (S x) X--)) (rewrite-l lzero (lsuc lzero) nat (times m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S x) (times m n)) (le (S x) X--)) (refl (lsuc lzero) (Set (lzero)) (le (S x) (times m n))) (plus O (times m n)) (plus-O-n (times m n))) (plus (times m n) O) (commutative-plus (times m n) O)))) (eq-ind-r lzero lzero bool true (λ (x0 : bool) -> λ (X-- : eq lzero bool x0 true) -> eq lzero bool (andb x0 (eqb (mod x n) b)) true) (eq-ind-r lzero lzero bool true (λ (x0 : bool) -> λ (X-- : eq lzero bool x0 true) -> eq lzero bool (andb true x0) true) (refl lzero bool (andb true true)) (eqb (mod x n) b) (eq-to-eqb-true (mod x n) b (eq-ind lzero lzero nat (mod b n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (mod b n) x-1) -> eq lzero nat (mod x n) x-1) (rewrite-r lzero lzero nat (mod b n) (λ (X-- : nat) -> eq lzero nat X-- (mod b n)) (refl lzero nat (mod b n)) (mod x n) cxb) b (lt-to-eq-mod b n ltbn)))) (eqb (mod x m) a) (eq-to-eqb-true (mod x m) a (eq-ind lzero lzero nat (mod a m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (mod a m) x-1) -> eq lzero nat (mod x m) x-1) (rewrite-r lzero lzero nat (mod a m) (λ (X-- : nat) -> eq lzero nat X-- (mod a m)) (refl lzero nat (mod a m)) (mod x m) cxa) a (lt-to-eq-mod a m ltam)))))) X-clearme0) X-clearme) (congruent-ab-lt m n a b (le-to-lt-to-lt O b n (le-O-n b) ltbn) (le-to-lt-to-lt O a m (le-O-n a) ltam) pnm)))))