|
405
|
1 {-# OPTIONS --cubical-compatible --safe #-}
|
|
|
2
|
|
57
|
3 module root2 where
|
|
|
4
|
|
141
|
5 open import Data.Nat
|
|
|
6 open import Data.Nat.Properties
|
|
57
|
7 open import Data.Empty
|
|
141
|
8 open import Data.Unit using (⊤ ; tt)
|
|
57
|
9 open import Relation.Nullary
|
|
|
10 open import Relation.Binary.PropositionalEquality
|
|
141
|
11 open import Relation.Binary.Definitions
|
|
57
|
12
|
|
281
|
13 import gcd as GCD
|
|
159
|
14 open import even
|
|
142
|
15 open import nat
|
|
231
|
16 open import logic
|
|
141
|
17
|
|
|
18 record Rational : Set where
|
|
|
19 field
|
|
|
20 i j : ℕ
|
|
320
|
21 0<j : j > 0
|
|
281
|
22 coprime : GCD.gcd i j ≡ 1
|
|
|
23
|
|
|
24 -- record Dividable (n m : ℕ ) : Set where
|
|
|
25 -- field
|
|
|
26 -- factor : ℕ
|
|
|
27 -- is-factor : factor * n + 0 ≡ m
|
|
|
28
|
|
|
29 gcd : (i j : ℕ) → ℕ
|
|
|
30 gcd = GCD.gcd
|
|
|
31
|
|
|
32 gcd-euclid : ( p a b : ℕ ) → 1 < p → 0 < a → 0 < b → ((i : ℕ ) → i < p → 0 < i → gcd p i ≡ 1)
|
|
|
33 → Dividable p (a * b) → Dividable p a ∨ Dividable p b
|
|
|
34 gcd-euclid = GCD.gcd-euclid
|
|
|
35
|
|
|
36 gcd-div1 : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j )
|
|
|
37 → Dividable k ( gcd i j )
|
|
|
38 gcd-div1 = GCD.gcd-div
|
|
57
|
39
|
|
231
|
40 open _∧_
|
|
|
41
|
|
|
42 open import prime
|
|
|
43
|
|
233
|
44 divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n
|
|
|
45 divdable^2 zero zero () 1<n pk dn2
|
|
|
46 divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
|
|
159
|
47 ... | yes y = y
|
|
250
|
48 ... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2
|
|
233
|
49 ... | case1 dn = dn
|
|
|
50 ... | case2 dm = dm
|
|
159
|
51
|
|
330
|
52 -- divdable-n*m : { n m k : ℕ } → 1 < k → 1 < n → Prime k → Dividable k ( n * m ) → Dividable k n ∨ Dividable k n
|
|
|
53 -- divdable-n*m = ?
|
|
|
54
|
|
|
55 -- 2^2 : { n k : ℕ } → 1 < n → Dividable 2 ( n * n ) → Dividable 2 n
|
|
|
56 -- 2^2 = ?
|
|
|
57
|
|
255
|
58 -- p * n * n ≡ m * m means (m/n)^2 = p
|
|
|
59 -- rational m/n requires m and n is comprime each other which contradicts the condition
|
|
|
60
|
|
254
|
61 root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime p → m > 1 → p * n * n ≡ m * m → ¬ (gcd n m ≡ 1)
|
|
|
62 root-prime-irrational n m 0 n>1 pn m>1 pnm = ⊥-elim ( nat-≡< refl (<-trans a<sa (Prime.p>1 pn)))
|
|
281
|
63 root-prime-irrational n m (suc p0) n>1 pn m>1 pnm = rot13 ( gcd-div1 n m (suc p0) 1<sp dn dm ) where
|
|
|
64 p = suc p0
|
|
254
|
65 1<sp : 1 < p
|
|
253
|
66 1<sp = Prime.p>1 pn
|
|
281
|
67 rot13 : {m : ℕ } → Dividable (suc p0) m → m ≡ 1 → ⊥
|
|
185
|
68 rot13 d refl with Dividable.factor d | Dividable.is-factor d
|
|
253
|
69 ... | zero | () -- gcd 0 m ≡ 1
|
|
254
|
70 ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * p + 0) ≡ 1
|
|
281
|
71 rot17 : suc n * (suc p0) + 0 > 1
|
|
253
|
72 rot17 = begin
|
|
|
73 2 ≡⟨ refl ⟩
|
|
254
|
74 suc (1 * 1 ) ≤⟨ 1<sp ⟩
|
|
|
75 suc p0 ≡⟨ cong suc (+-comm 0 _) ⟩
|
|
|
76 suc (p0 + 0) ≤⟨ s≤s (+-monoʳ-≤ p0 z≤n) ⟩
|
|
|
77 suc (p0 + n * p ) ≡⟨ +-comm 0 _ ⟩
|
|
|
78 suc n * p + 0 ∎ where open ≤-Reasoning
|
|
|
79 dm : Dividable p m
|
|
|
80 dm = divdable^2 m p 1<sp m>1 pn record { factor = n * n ; is-factor = begin
|
|
|
81 (n * n) * p + 0 ≡⟨ +-comm _ 0 ⟩
|
|
|
82 (n * n) * p ≡⟨ *-comm (n * n) p ⟩
|
|
|
83 p * (n * n) ≡⟨ sym (*-assoc p n n) ⟩
|
|
|
84 (p * n) * n ≡⟨ pnm ⟩
|
|
250
|
85 m * m ∎ } where open ≡-Reasoning
|
|
254
|
86 -- p * n * n = 2m' 2m'
|
|
251
|
87 -- n * n = m' 2m'
|
|
250
|
88 df = Dividable.factor dm
|
|
254
|
89 dn : Dividable p n
|
|
|
90 dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df ; is-factor = begin
|
|
405
|
91 df * df * p + 0 ≡⟨ *-cancelʳ-≡ _ _ (suc p0) ( begin
|
|
254
|
92 (df * df * p + 0) * p ≡⟨ cong (λ k → k * p) (+-comm (df * df * p) 0) ⟩
|
|
281
|
93 ((df * df) * p ) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩
|
|
254
|
94 (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p) ⟩
|
|
|
95 (df * (p * df)) * p ≡⟨ sym ( cong (λ k → k * p) (*-assoc df p df ) ) ⟩
|
|
|
96 ((df * p) * df) * p ≡⟨ *-assoc (df * p) df p ⟩
|
|
|
97 (df * p) * (df * p) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * p)) (+-comm 0 _) ⟩
|
|
|
98 (df * p + 0) * (df * p + 0) ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
|
|
253
|
99 m * m ≡⟨ sym pnm ⟩
|
|
281
|
100 p * n * n ≡⟨ cong (λ k → k * n) (*-comm p n) ⟩
|
|
|
101 n * p * n ≡⟨ *-assoc n p n ⟩
|
|
|
102 n * (p * n) ≡⟨ cong (λ k → n * k) (*-comm p n) ⟩
|
|
|
103 n * (n * p) ≡⟨ sym (*-assoc n n p) ⟩
|
|
254
|
104 n * n * p ∎ ) ⟩
|
|
250
|
105 n * n ∎ } where open ≡-Reasoning
|
|
57
|
106
|
|
320
|
107 mkRational : ( i j : ℕ ) → 0 < j → Rational
|
|
|
108 mkRational zero j 0<j = record { i = 0 ; j = 1 ; coprime = refl ; 0<j = s≤s z≤n }
|
|
321
|
109 mkRational (suc i) (suc j) (s≤s 0<j) = record { i = Dividable.factor id ; j = Dividable.factor jd ; coprime = cop ; 0<j = 0<fj } where
|
|
320
|
110 d : ℕ
|
|
321
|
111 d = gcd (suc i) (suc j)
|
|
|
112 d>0 : gcd (suc i) (suc j) > 0
|
|
|
113 d>0 = GCD.gcd>0 (suc i) (suc j) (s≤s z≤n) (s≤s z≤n )
|
|
|
114 id : Dividable d (suc i)
|
|
|
115 id = proj1 (GCD.gcd-dividable (suc i) (suc j))
|
|
|
116 jd : Dividable d (suc j)
|
|
|
117 jd = proj2 (GCD.gcd-dividable (suc i) (suc j))
|
|
320
|
118 0<fj : Dividable.factor jd > 0
|
|
|
119 0<fj = 0<factor d>0 (s≤s z≤n ) jd
|
|
|
120 cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1
|
|
321
|
121 cop = GCD.gcd-div-1 {suc i} {suc j} (s≤s z≤n) (s≤s z≤n )
|
|
320
|
122
|
|
321
|
123 r1 : {x y : ℕ} → x > 0 → y > 0 → x * y > 0
|
|
|
124 r1 {x} {y} x>0 y>0 = begin
|
|
320
|
125 1 * 1 ≤⟨ *≤ {1} {x} {1} x>0 ⟩
|
|
|
126 x * 1 ≡⟨ *-comm x 1 ⟩
|
|
|
127 1 * x ≤⟨ *≤ {1} {y} {x} y>0 ⟩
|
|
|
128 y * x ≡⟨ *-comm y x ⟩
|
|
|
129 x * y ∎ where open ≤-Reasoning
|
|
185
|
130
|
|
321
|
131 Rational* : (r s : Rational) → Rational
|
|
|
132 Rational* r s = mkRational (Rational.i r * Rational.i s) (Rational.j r * Rational.j s) (r1 (Rational.0<j r) (Rational.0<j s) )
|
|
|
133
|
|
281
|
134 _r=_ : Rational → ℕ → Set
|
|
321
|
135 r r= p = p * Rational.j r ≡ Rational.i r
|
|
|
136
|
|
|
137 r3 : ( p : ℕ ) → p > 0 → ( r : Rational ) → Rational* r r r= p → p * Rational.j r * Rational.j r ≡ Rational.i r * Rational.i r
|
|
|
138 r3 p p>0 r rr = r4 where
|
|
|
139 i : ℕ
|
|
|
140 i = Rational.i r * Rational.i r
|
|
|
141 j : ℕ
|
|
|
142 j = Rational.j r * Rational.j r
|
|
|
143 0<j : 0 < j
|
|
|
144 0<j = r1 (Rational.0<j r) (Rational.0<j r)
|
|
|
145 d1 = Dividable.factor (proj1 (GCD.gcd-dividable i j))
|
|
|
146 d2 = Dividable.factor (proj2 (GCD.gcd-dividable i j))
|
|
|
147 ri=id : ( i j : ℕ) → (0<i : 0 < i ) → (0<j : 0 < j)
|
|
|
148 → Rational.i (mkRational i j 0<j) ≡ Dividable.factor (proj1 (GCD.gcd-dividable i j))
|
|
|
149 ri=id (suc i₁) (suc j₁) 0<i (s≤s 0<j₁) = refl
|
|
|
150 ri=jd : ( i j : ℕ) → (0<i : 0 < i ) → (0<j : 0 < j)
|
|
|
151 → Rational.j (mkRational i j 0<j) ≡ Dividable.factor (proj2 (GCD.gcd-dividable i j))
|
|
|
152 ri=jd (suc i₁) (suc j₁) 0<i (s≤s 0<j₁) = refl
|
|
322
|
153 r0=id : ( i j : ℕ) → (0=i : 0 ≡ i ) → (0<j : 0 < j)
|
|
|
154 → Rational.i (mkRational i j 0<j) ≡ 0
|
|
|
155 r0=id 0 j refl 0<j = refl
|
|
|
156 r0=jd : ( i j : ℕ) → (0=i : 0 ≡ i ) → (0<j : 0 < j)
|
|
|
157 → Rational.j (mkRational i j 0<j) ≡ 1
|
|
|
158 r0=jd 0 j refl 0<j = refl
|
|
321
|
159 d : ℕ
|
|
|
160 d = gcd i j
|
|
|
161 r7 : i > 0 → d > 0
|
|
|
162 r7 0<i = GCD.gcd>0 _ _ 0<i 0<j
|
|
|
163 r6 : i > 0 → d2 > 0
|
|
|
164 r6 0<i = 0<factor (r7 0<i ) 0<j (proj2 (GCD.gcd-dividable i j))
|
|
|
165 r8 : 0 < i → d2 * p ≡ d1
|
|
|
166 r8 0<i = begin
|
|
|
167 d2 * p ≡⟨ *-comm d2 p ⟩
|
|
|
168 p * d2 ≡⟨ cong (λ k → p * k ) (sym (ri=jd i j 0<i 0<j )) ⟩
|
|
|
169 p * Rational.j (mkRational i j _ ) ≡⟨ rr ⟩
|
|
|
170 Rational.i (Rational* r r) ≡⟨ ri=id i j 0<i 0<j ⟩
|
|
|
171 d1 ∎ where open ≡-Reasoning
|
|
|
172 r4 : p * Rational.j r * Rational.j r ≡ Rational.i r * Rational.i r
|
|
|
173 r4 with <-cmp (Rational.i r * Rational.i r) 0
|
|
322
|
174 ... | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< (begin
|
|
|
175 0 ≡⟨ sym (r0=id i j (sym b) 0<j ) ⟩
|
|
|
176 Rational.i (mkRational (Rational.i r * Rational.i r) (Rational.j r * Rational.j r) _ ) ≡⟨ sym rr ⟩
|
|
|
177 p * Rational.j (mkRational (Rational.i r * Rational.i r) (Rational.j r * Rational.j r) _ ) ≡⟨ cong (λ k → p * k ) (r0=jd i j (sym b) 0<j ) ⟩
|
|
|
178 p * 1 ≡⟨ m*1=m ⟩
|
|
|
179 p ∎ ) p>0 ) where open ≡-Reasoning
|
|
321
|
180 ... | tri> ¬a ¬b c = begin
|
|
|
181 p * Rational.j r * Rational.j r ≡⟨ *-cancel-left (r6 c) ( begin
|
|
322
|
182 d2 * ((p * Rational.j r) * Rational.j r) ≡⟨ sym (*-assoc d2 _ _) ⟩
|
|
|
183 (d2 * ( p * Rational.j r )) * Rational.j r ≡⟨ cong (λ k → k * Rational.j r) (sym (*-assoc d2 _ _ )) ⟩
|
|
321
|
184 (d2 * p) * Rational.j r * Rational.j r ≡⟨ cong (λ k → k * Rational.j r * Rational.j r) (r8 c) ⟩
|
|
|
185 d1 * Rational.j r * Rational.j r ≡⟨ *-cancel-left (r7 c) ( begin
|
|
322
|
186 d * ((d1 * Rational.j r) * Rational.j r) ≡⟨ cong (λ k → d * k ) (*-assoc d1 _ _ )⟩
|
|
|
187 d * (d1 * (Rational.j r * Rational.j r)) ≡⟨ sym (*-assoc d _ _) ⟩
|
|
|
188 (d * d1) * (Rational.j r * Rational.j r) ≡⟨ cong (λ k → k * j) (*-comm d _ ) ⟩
|
|
|
189 (d1 * d) * j ≡⟨ cong (λ k → k * j) (+-comm 0 (d1 * d) ) ⟩
|
|
321
|
190 (d1 * d + 0) * j ≡⟨ cong (λ k → k * j ) (Dividable.is-factor (proj1 (GCD.gcd-dividable i j)) ) ⟩
|
|
|
191 i * j ≡⟨ *-comm i j ⟩
|
|
|
192 j * i ≡⟨ cong (λ k → k * i ) (sym (Dividable.is-factor (proj2 (GCD.gcd-dividable i j))) ) ⟩
|
|
322
|
193 (d2 * GCD.gcd i j + 0) * i ≡⟨ cong (λ k → k * i ) (+-comm (d2 * d ) 0) ⟩
|
|
|
194 (d2 * d) * i ≡⟨ cong (λ k → k * i ) (*-comm d2 _ ) ⟩
|
|
|
195 (d * d2) * i ≡⟨ *-assoc d _ _ ⟩
|
|
321
|
196 d * (d2 * (Rational.i r * Rational.i r)) ∎ ) ⟩
|
|
|
197 d2 * (Rational.i r * Rational.i r) ∎ ) ⟩
|
|
|
198 Rational.i r * Rational.i r ∎ where open ≡-Reasoning
|
|
|
199
|
|
325
|
200 *<-2 : {x y z : ℕ} → z > 0 → x < y → z * x < z * y
|
|
405
|
201 *<-2 {x} {y} {suc z} (s≤s z>0) x<y = ? -- *-monoʳ-< z x<y
|
|
325
|
202
|
|
|
203 r15 : {p : ℕ} → p > 1 → p < p * p
|
|
|
204 r15 {p} p>1 = subst (λ k → k < p * p ) m*1=m (*<-2 (<-trans a<sa p>1) p>1 )
|
|
281
|
205
|
|
320
|
206 root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r : Rational ) → ¬ ( Rational* r r r= p )
|
|
321
|
207 root-prime-irrational1 p pr r div with <-cmp (Rational.j r) 1
|
|
|
208 ... | tri> ¬a ¬b c with <-cmp (Rational.i r) 1
|
|
325
|
209 ... | tri> ¬a₁ ¬b₁ c₁ = root-prime-irrational (Rational.j r) (Rational.i r) p c pr c₁ (r3 p (<-trans a<sa (Prime.p>1 pr ) ) r div)
|
|
|
210 (trans (GCD.gcdsym {Rational.j r} {_} ) (Rational.coprime r) )
|
|
324
|
211 ... | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≡< (sym r05) r08) where
|
|
322
|
212 i = Rational.i r
|
|
|
213 j = Rational.j r
|
|
|
214 r00 : p * j * j ≡ i * i
|
|
|
215 r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
|
|
|
216 r06 : i ≡ 0
|
|
324
|
217 r06 with <-cmp i 0
|
|
|
218 ... | tri≈ ¬a b ¬c = b
|
|
|
219 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c a )
|
|
|
220 r05 : p * j * j ≡ 0
|
|
325
|
221 r05 with r06
|
|
|
222 ... | refl = r00
|
|
|
223 r09 : p * j > 0
|
|
|
224 r09 = begin
|
|
|
225 suc zero ≤⟨ <-trans a<sa (Prime.p>1 pr) ⟩
|
|
|
226 p ≡⟨ sym m*1=m ⟩
|
|
|
227 p * 1 <⟨ *<-2 (<-trans a<sa (Prime.p>1 pr)) c ⟩
|
|
|
228 p * j ∎ where open ≤-Reasoning
|
|
324
|
229 r08 : p * j * j > 0
|
|
325
|
230 r08 = begin
|
|
|
231 suc zero ≤⟨ r09 ⟩
|
|
|
232 p * j ≡⟨ sym m*1=m ⟩
|
|
|
233 (p * j) * 1 <⟨ *<-2 r09 c ⟩
|
|
|
234 (p * j) * j ∎ where open ≤-Reasoning
|
|
324
|
235 ... | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< (sym r07) r09) where
|
|
322
|
236 i = Rational.i r
|
|
|
237 j = Rational.j r
|
|
|
238 r00 : p * j * j ≡ i * i
|
|
|
239 r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
|
|
324
|
240 r07 : p * j * j ≡ 1
|
|
325
|
241 r07 = begin
|
|
|
242 p * j * j ≡⟨ r00 ⟩
|
|
|
243 i * i ≡⟨ cong (λ k → k * k) b ⟩
|
|
|
244 1 * 1 ≡⟨⟩
|
|
|
245 1 ∎ where open ≡-Reasoning
|
|
|
246 r19 : 1 < p * j
|
|
|
247 r19 = begin
|
|
|
248 suc 1 ≤⟨ Prime.p>1 pr ⟩
|
|
|
249 p ≡⟨ sym m*1=m ⟩
|
|
|
250 p * 1 <⟨ *<-2 (<-trans a<sa (Prime.p>1 pr)) c ⟩
|
|
|
251 p * j ∎ where open ≤-Reasoning
|
|
324
|
252 r09 : 1 < p * j * j
|
|
325
|
253 r09 = begin
|
|
|
254 suc 1 ≤⟨ r19 ⟩
|
|
|
255 p * j ≡⟨ sym m*1=m ⟩
|
|
|
256 p * j * 1 <⟨ *<-2 (<-trans a<sa r19 ) c ⟩
|
|
|
257 (p * j) * j ∎ where open ≤-Reasoning
|
|
|
258 root-prime-irrational1 p pr r div | tri< a ¬b ¬c = ⊥-elim (nat-≤> (Rational.0<j r) a )
|
|
|
259 root-prime-irrational1 p pr r div | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< r04 (r03 r01)) where
|
|
|
260 i = Rational.i r
|
|
|
261 j = Rational.j r
|
|
|
262 p>0 : p > 0
|
|
|
263 p>0 = <-trans a<sa (Prime.p>1 pr)
|
|
|
264 r00 : p * j * j ≡ i * i
|
|
|
265 r00 = r3 p p>0 r div
|
|
|
266 r01 : p ≡ i * i
|
|
|
267 r01 = begin
|
|
|
268 p ≡⟨ sym m*1=m ⟩
|
|
|
269 p * 1 ≡⟨ sym m*1=m ⟩
|
|
|
270 p * 1 * 1 ≡⟨ cong (λ k → p * k * k ) (sym b) ⟩
|
|
|
271 p * j * j ≡⟨ r00 ⟩
|
|
|
272 i * i ∎ where open ≡-Reasoning
|
|
|
273 r03 : p ≡ i * i → i > 1
|
|
|
274 r03 eq with <-cmp i 1
|
|
|
275 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym r11) p>0 ) where
|
|
|
276 r10 : i ≡ 0
|
|
|
277 r10 with <-cmp i 0
|
|
|
278 ... | tri≈ ¬a b ¬c = b
|
|
|
279 ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c a )
|
|
|
280 r11 : p ≡ 0
|
|
|
281 r11 = begin
|
|
|
282 p ≡⟨ r01 ⟩
|
|
|
283 i * i ≡⟨ cong (λ k → k * k ) r10 ⟩
|
|
|
284 0 * 0 ≡⟨⟩
|
|
|
285 0 ∎ where open ≡-Reasoning
|
|
|
286 ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< (sym r01 ) (Prime.p>1 pr))
|
|
|
287 ... | tri> ¬a ¬b c = c
|
|
|
288 r02 : p ≡ i * i → gcd p i ≡ i
|
|
|
289 r02 eq = GCD.div→gcd (r03 r01) record { factor = i ; is-factor = trans (+-comm _ 0 ) (sym r01) }
|
|
|
290 r14 : i < p
|
|
|
291 r14 with <-cmp i p
|
|
|
292 ... | tri< a ¬b ¬c = a
|
|
|
293 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< r01 (begin
|
|
|
294 suc p ≤⟨ r15 (Prime.p>1 pr) ⟩
|
|
|
295 p * p ≡⟨ cong (λ k → k * k ) (sym b) ⟩
|
|
|
296 i * i ∎ )) where open ≤-Reasoning
|
|
|
297 ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< r01 (<-trans c (r15 (r03 r01 ))))
|
|
|
298 r04 : 1 ≡ i
|
|
|
299 r04 = begin
|
|
|
300 1 ≡⟨ sym (Prime.isPrime pr _ r14 (<-trans a<sa (r03 r01 ))) ⟩
|
|
|
301 gcd p i ≡⟨ r02 r01 ⟩
|
|
|
302 i ∎ where open ≡-Reasoning
|
