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