Skip to content

Commit 77847c7

Browse files
LorenzoMolenaLorenzoMolena
committed
update GCD with the more efficient implementation
1 parent e6fdcc9 commit 77847c7

File tree

2 files changed

+304
-34
lines changed

2 files changed

+304
-34
lines changed

‎Cubical/Data/Nat/GCD.agda‎

Lines changed: 137 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -9,14 +9,17 @@ open import Cubical.Foundations.Isomorphism
99
open import Cubical.Induction.WellFounded
1010

1111
open import Cubical.Data.Sigma as Σ
12-
open import Cubical.Data.Fin
12+
open import Cubical.Data.Fin as F hiding (_%_ ; _/_)
1313
open import Cubical.Data.NatPlusOne
1414

1515
open import Cubical.HITs.PropositionalTruncation as PropTrunc
1616

1717
open import Cubical.Data.Nat.Base
1818
open import Cubical.Data.Nat.Properties
1919
open import Cubical.Data.Nat.Order
20+
open import Cubical.Data.Nat.Mod renaming (
21+
quotient'_/_ to _/_ ; remainder'_/_ to _%_
22+
; ≡remainder'+quotient' to ≡%+·/ ; mod'< to %< )
2023
open import Cubical.Data.Nat.Divisibility
2124

2225
open import Cubical.Relation.Nullary
@@ -66,46 +69,94 @@ oneGCD m = symGCD (divsGCD (∣-oneˡ m))
6669
zeroGCD : ∀ m → isGCD m 0 m
6770
zeroGCD m = divsGCD (∣-zeroʳ m)
6871

72+
-- a pair of useful lemmas about ∣ and (efficient) %
6973
private
70-
lem₁ : prediv d (suc n) → prediv d (m % suc n) → prediv d m
71-
lem₁ {d} {n} {m} (c₁ , p₁) (c₂ , p₂) = (q · c₁ + c₂) , p
72-
where r = m % suc n; q = n%k≡n[modk] m (suc n) .fst
73-
p = (q · c₁ + c₂) · d ≡⟨ sym (·-distribʳ (q · c₁) c₂ d) ⟩
74-
(q · c₁) · d + c₂ · d ≡⟨ cong (_+ c₂ · d) (sym (·-assoc q c₁ d)) ⟩
75-
q · (c₁ · d) + c₂ · d ≡[ i ]⟨ q · (p₁ i) + (p₂ i) ⟩
76-
q · (suc n) + r ≡⟨ n%k≡n[modk] m (suc n) .snd ⟩
77-
m ∎
78-
79-
lem₂ : prediv d (suc n) → prediv d m → prediv d (m % suc n)
80-
lem₂ {d} {n} {m} (c₁ , p₁) (c₂ , p₂) = c₂ ∸ q · c₁ , p
81-
where r = m % suc n; q = n%k≡n[modk] m (suc n) .fst
82-
p = (c₂ ∸ q · c₁) · d ≡⟨ ∸-distribʳ c₂ (q · c₁) d ⟩
83-
c₂ · d ∸ (q · c₁) · d ≡⟨ cong (c₂ · d ∸_) (sym (·-assoc q c₁ d)) ⟩
84-
c₂ · d ∸ q · (c₁ · d) ≡[ i ]⟨ p₂ i ∸ q · (p₁ i) ⟩
85-
m ∸ q · (suc n) ≡⟨ cong (_∸ q · (suc n)) (sym (n%k≡n[modk] m (suc n) .snd)) ⟩
86-
(q · (suc n) + r) ∸ q · (suc n) ≡⟨ cong (_∸ q · (suc n)) (+-comm (q · (suc n)) r) ⟩
87-
(r + q · (suc n)) ∸ q · (suc n) ≡⟨ ∸-cancelʳ r zero (q · (suc n)) ⟩
88-
r ∎
74+
∣→∣% : ∀ {m n d} → d ∣ m → d ∣ n → d ∣ (m % n)
75+
∣%→∣ : ∀ {m n d} → d ∣ (m % n) → d ∣ n → d ∣ m
76+
77+
∣→∣% {m} {0} {d} d∣m d∣n = d∣m
78+
∣→∣% {m} {n@(suc _)} {d} d∣m d∣n =
79+
let
80+
k₁ = ∣-untrunc d∣m .fst
81+
k₁·d≡m = ∣-untrunc d∣m .snd
82+
k₂ = ∣-untrunc d∣n .fst
83+
k₂·d≡n = ∣-untrunc d∣n .snd
84+
p =
85+
(k₁ ∸ m / n · k₂) · d ≡⟨ ∸-distribʳ k₁ (m / n · k₂) d ⟩
86+
k₁ · d ∸ m / n · k₂ · d ≡⟨ sym $ cong (k₁ · d ∸_) (·-assoc (m / n) _ _) ⟩
87+
k₁ · d ∸ m / n · (k₂ · d) ≡⟨ cong₂ (λ l r → l ∸ m / n · r) k₁·d≡m k₂·d≡n ⟩
88+
m ∸ m / n · n ≡⟨ cong (m ∸_) (·-comm (m / n) n) ⟩
89+
m ∸ n · m / n ≡⟨ sym $ cong (_∸ n · m / n) (≡%+·/ n m) ⟩
90+
m % n + n · m / n ∸ n · m / n ≡⟨ +∸ (m % n) (n · m / n) ⟩
91+
m % n ∎
92+
in
93+
∣ k₁ ∸ m / n · k₂ , p ∣₁
94+
95+
∣%→∣ {m} {0} {d} d∣m%n d∣n = d∣m%n
96+
∣%→∣ {m} {n@(suc _)} {d} d∣m%n d∣n =
97+
let
98+
k₁ = ∣-untrunc d∣m%n .fst
99+
k₁·d≡m%n = ∣-untrunc d∣m%n .snd
100+
k₂ = ∣-untrunc d∣n .fst
101+
k₂·d≡n = ∣-untrunc d∣n .snd
102+
p =
103+
(k₁ + k₂ · m / n) · d ≡⟨ sym $ ·-distribʳ k₁ (k₂ · m / n) d ⟩
104+
k₁ · d + k₂ · m / n · d ≡⟨ cong (λ p → k₁ · d + p · d) (·-comm k₂ (m / n)) ⟩
105+
k₁ · d + m / n · k₂ · d ≡⟨ sym $ cong (k₁ · d +_) (·-assoc (m / n) k₂ d) ⟩
106+
k₁ · d + m / n · (k₂ · d) ≡⟨ cong₂ (λ l r → l + m / n · r) k₁·d≡m%n k₂·d≡n ⟩
107+
m % n + m / n · n ≡⟨ cong (m % n +_) (·-comm (m / n) n) ⟩
108+
m % n + n · m / n ≡⟨ ≡%+·/ n m ⟩
109+
m ∎
110+
in
111+
∣ k₁ + k₂ · m / n , p ∣₁
89112

90113
-- The inductive step of the Euclidean algorithm
91114
stepGCD : isGCD (suc n) (m % suc n) d
92115
→ isGCD m (suc n) d
93-
fst (stepGCD ((d∣n , d∣m%n) , gr)) = PropTrunc.map2 lem₁ d∣n d∣m%n , d∣n
94-
snd (stepGCD ((d∣n , d∣m%n) , gr)) d' (d'∣m , d'∣n) = gr d' (d'∣n , PropTrunc.map2 lem₂ d'∣n d'∣m)
95-
96-
-- putting it all together using well-founded induction
97-
98-
euclid< : ∀ m n → n < m → GCD m n
99-
euclid< = WFI.induction <-wellfounded λ {
100-
m rec zero p → m , zeroGCD m ;
101-
m rec (suc n) p → let d , dGCD = rec (suc n) p (m % suc n) (n%sk<sk m n)
102-
in d , stepGCD dGCD }
116+
stepGCD w =
117+
let
118+
g∣1+n = w .fst .fst
119+
g∣m%1+n = w .fst .snd
120+
d∣1+n→d∣m%1+n→d∣g = w .snd
121+
in
122+
(∣%→∣ g∣m%1+n g∣1+n , g∣1+n) ,
123+
λ d' (d'∣m , d'∣1+n) → d∣1+n→d∣m%1+n→d∣g d' (d'∣1+n , (∣→∣% d'∣m d'∣1+n))
124+
125+
-- putting it all together using an auxiliary variable to pass the termination checking
126+
127+
euclid-helper< : (m n f : ℕ) → (n < m) → (m ≤ f) → GCD m n
128+
euclid-helper< m n zero n<m m≤0 .fst = 0
129+
euclid-helper< m n zero n<m m≤0 .snd .fst .fst = ∣-refl $ sym $ ≤0→≡0 m≤0
130+
euclid-helper< m n zero n<m m≤0 .snd .fst .snd = ∣-refl $ sym $ ≤0→≡0 $
131+
<-weaken $ <≤-trans n<m m≤0
132+
euclid-helper< m n zero n<m m≤0 .snd .snd d' _ = ∣-zeroʳ d'
133+
euclid-helper< zero zero (suc _) _ _ .fst = 0
134+
euclid-helper< zero zero (suc _) _ _ .snd .fst .fst = ∣-refl refl
135+
euclid-helper< zero zero (suc _) _ _ .snd .fst .snd = ∣-refl refl
136+
euclid-helper< zero zero (suc _) _ _ .snd .snd d' _ = ∣-zeroʳ d'
137+
euclid-helper< zero (suc n) (suc _) _ _ .fst = suc n
138+
euclid-helper< zero (suc n) (suc _) _ _ .snd .fst .fst = ∣-zeroʳ (suc n)
139+
euclid-helper< zero (suc n) (suc _) _ _ .snd .fst .snd = ∣-refl refl
140+
euclid-helper< zero (suc n) (suc _) _ _ .snd .snd d' (_ , d'∣1+n) = d'∣1+n
141+
euclid-helper< (suc m) zero (suc _) _ _ .fst = suc m
142+
euclid-helper< (suc m) zero (suc _) _ _ .snd .fst .fst = ∣-refl refl
143+
euclid-helper< (suc m) zero (suc _) _ _ .snd .fst .snd = ∣-zeroʳ (suc m)
144+
euclid-helper< (suc m) zero (suc _) _ _ .snd .snd d' (d'∣1+m , _) = d'∣1+m
145+
euclid-helper< m@(suc _) n@(suc n-1) (suc f) n<m m≤1+f =
146+
let
147+
n≤f = predℕ-≤-predℕ $ <≤-trans n<m m≤1+f
148+
r = euclid-helper< n (m % n) f (%< n-1 m) n≤f
149+
in
150+
r .fst , stepGCD (r .snd)
103151

104152
euclid : ∀ m n → GCD m n
105-
euclid m n with n ≟ m
106-
... | lt p = euclid< m n p
107-
... | gt p = Σ.map-snd symGCD (euclid< n m p)
108-
... | eq p = m , divsGCD (∣-refl (sym p))
153+
euclid m zero = m , (∣-refl refl , ∣-zeroʳ m) , λ d' (d'∣m , _) → d'∣m
154+
euclid m n@(suc n-1) =
155+
let
156+
r = euclid-helper< n (m % n) n (%< n-1 m) ≤-refl
157+
in
158+
r .fst , stepGCD (r .snd)
159+
109160

110161
isContrGCD : ∀ m n → isContr (GCD m n)
111162
isContrGCD m n = euclid m n , isPropGCD _
@@ -165,3 +216,55 @@ isGCD-multʳ {m} {n} {d} k dGCD = gcd≡→isGCD (gcd-factorʳ m n k ∙ cong (_
165216

166217
stDivIneqGCD : ¬ m ≡ 0 → ¬ m ∣ n → (g : GCD m n) → g .fst < m
167218
stDivIneqGCD p q g = stDivIneq p q (g .snd .fst .fst) (g .snd .fst .snd)
219+
220+
-- Alternative definition of GCD using % from Cubical.Data.Fin and well-founded induction
221+
222+
private
223+
lem₁ : prediv d (suc n) → prediv d (m F.% suc n) → prediv d m
224+
lem₁ {d} {n} {m} (c₁ , p₁) (c₂ , p₂) = (q · c₁ + c₂) , p
225+
where r = m F.% suc n; q = n%k≡n[modk] m (suc n) .fst
226+
p = (q · c₁ + c₂) · d ≡⟨ sym (·-distribʳ (q · c₁) c₂ d) ⟩
227+
(q · c₁) · d + c₂ · d ≡⟨ cong (_+ c₂ · d) (sym (·-assoc q c₁ d)) ⟩
228+
q · (c₁ · d) + c₂ · d ≡[ i ]⟨ q · (p₁ i) + (p₂ i) ⟩
229+
q · (suc n) + r ≡⟨ n%k≡n[modk] m (suc n) .snd ⟩
230+
m ∎
231+
232+
lem₂ : prediv d (suc n) → prediv d m → prediv d (m F.% suc n)
233+
lem₂ {d} {n} {m} (c₁ , p₁) (c₂ , p₂) = c₂ ∸ q · c₁ , p
234+
where r = m F.% suc n; q = n%k≡n[modk] m (suc n) .fst
235+
p = (c₂ ∸ q · c₁) · d ≡⟨ ∸-distribʳ c₂ (q · c₁) d ⟩
236+
c₂ · d ∸ (q · c₁) · d ≡⟨ cong (c₂ · d ∸_) (sym (·-assoc q c₁ d)) ⟩
237+
c₂ · d ∸ q · (c₁ · d) ≡[ i ]⟨ p₂ i ∸ q · (p₁ i) ⟩
238+
m ∸ q · (suc n) ≡⟨ cong (_∸ q · (suc n)) (sym (n%k≡n[modk] m (suc n) .snd)) ⟩
239+
(q · (suc n) + r) ∸ q · (suc n) ≡⟨ cong (_∸ q · (suc n)) (+-comm (q · (suc n)) r) ⟩
240+
(r + q · (suc n)) ∸ q · (suc n) ≡⟨ ∸-cancelʳ r zero (q · (suc n)) ⟩
241+
r ∎
242+
243+
-- The inductive step of the Euclidean algorithm
244+
stepGCD' : isGCD (suc n) (m F.% suc n) d
245+
→ isGCD m (suc n) d
246+
fst (stepGCD' ((d∣n , d∣m%n) , gr)) = PropTrunc.map2 lem₁ d∣n d∣m%n , d∣n
247+
snd (stepGCD' ((d∣n , d∣m%n) , gr)) d' (d'∣m , d'∣n) = gr d' (d'∣n , PropTrunc.map2 lem₂ d'∣n d'∣m)
248+
249+
-- putting it all together using well-founded induction
250+
251+
euclid'< : ∀ m n → n < m → GCD m n
252+
euclid'< = WFI.induction <-wellfounded λ {
253+
m rec zero p → m , zeroGCD m ;
254+
m rec (suc n) p → let d , dGCD = rec (suc n) p (m F.% suc n) (n%sk<sk m n)
255+
in d , stepGCD' dGCD }
256+
257+
euclid' : ∀ m n → GCD m n
258+
euclid' m n with n ≟ m
259+
... | lt p = euclid'< m n p
260+
... | gt p = Σ.map-snd symGCD (euclid'< n m p)
261+
... | eq p = m , divsGCD (∣-refl (sym p))
262+
263+
gcd' : ℕ → ℕ → ℕ
264+
gcd' m n = euclid' m n .fst
265+
266+
euclid≡euclid' : ∀ m n → euclid m n ≡ euclid' m n
267+
euclid≡euclid' m n = isPropGCD (euclid m n) (euclid' m n)
268+
269+
gcd≡gcd' : ∀ m n → gcd m n ≡ gcd' m n
270+
gcd≡gcd' m n = cong fst (euclid≡euclid' m n)

‎Cubical/Data/Nat/InductiveGCD/GCD.agda‎

Lines changed: 167 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,167 @@
1+
module Cubical.Data.Nat.GCD where
2+
3+
open import Cubical.Foundations.Prelude
4+
open import Cubical.Foundations.Function
5+
open import Cubical.Foundations.HLevels
6+
open import Cubical.Foundations.Equiv
7+
open import Cubical.Foundations.Isomorphism
8+
9+
open import Cubical.Induction.WellFounded
10+
11+
open import Cubical.Data.Sigma as Σ
12+
open import Cubical.Data.Fin
13+
open import Cubical.Data.NatPlusOne
14+
15+
open import Cubical.HITs.PropositionalTruncation as PropTrunc
16+
17+
open import Cubical.Data.Nat.Base
18+
open import Cubical.Data.Nat.Properties
19+
open import Cubical.Data.Nat.Order
20+
open import Cubical.Data.Nat.Divisibility
21+
22+
open import Cubical.Relation.Nullary
23+
24+
private
25+
variable
26+
m n d : ℕ
27+
28+
-- common divisors
29+
30+
isCD : ℕ → ℕ → ℕ → Type₀
31+
isCD m n d = (d ∣ m) × (d ∣ n)
32+
33+
isPropIsCD : isProp (isCD m n d)
34+
isPropIsCD = isProp× isProp∣ isProp∣
35+
36+
symCD : isCD m n d → isCD n m d
37+
symCD (d∣m , d∣n) = (d∣n , d∣m)
38+
39+
-- greatest common divisors
40+
41+
isGCD : ℕ → ℕ → ℕ → Type₀
42+
isGCD m n d = (isCD m n d) × (∀ d' → isCD m n d' → d' ∣ d)
43+
44+
GCD : ℕ → ℕ → Type₀
45+
GCD m n = Σ ℕ (isGCD m n)
46+
47+
isPropIsGCD : isProp (isGCD m n d)
48+
isPropIsGCD = isProp× isPropIsCD (isPropΠ2 (λ _ _ → isProp∣))
49+
50+
isPropGCD : isProp (GCD m n)
51+
isPropGCD (d , dCD , gr) (d' , d'CD , gr') =
52+
Σ≡Prop (λ _ → isPropIsGCD) (antisym∣ (gr' d dCD) (gr d' d'CD))
53+
54+
55+
symGCD : isGCD m n d → isGCD n m d
56+
symGCD (dCD , gr) = symCD dCD , λ { d' d'CD → gr d' (symCD d'CD) }
57+
58+
divsGCD : m ∣ n → isGCD m n m
59+
divsGCD p = (∣-refl refl , p) , λ { d (d∣m , _) → d∣m }
60+
61+
oneGCD : ∀ m → isGCD m 1 1
62+
oneGCD m = symGCD (divsGCD (∣-oneˡ m))
63+
64+
65+
-- The base case of the Euclidean algorithm
66+
zeroGCD : ∀ m → isGCD m 0 m
67+
zeroGCD m = divsGCD (∣-zeroʳ m)
68+
69+
private
70+
lem₁ : prediv d (suc n) → prediv d (m % suc n) → prediv d m
71+
lem₁ {d} {n} {m} (c₁ , p₁) (c₂ , p₂) = (q · c₁ + c₂) , p
72+
where r = m % suc n; q = n%k≡n[modk] m (suc n) .fst
73+
p = (q · c₁ + c₂) · d ≡⟨ sym (·-distribʳ (q · c₁) c₂ d) ⟩
74+
(q · c₁) · d + c₂ · d ≡⟨ cong (_+ c₂ · d) (sym (·-assoc q c₁ d)) ⟩
75+
q · (c₁ · d) + c₂ · d ≡[ i ]⟨ q · (p₁ i) + (p₂ i) ⟩
76+
q · (suc n) + r ≡⟨ n%k≡n[modk] m (suc n) .snd ⟩
77+
m ∎
78+
79+
lem₂ : prediv d (suc n) → prediv d m → prediv d (m % suc n)
80+
lem₂ {d} {n} {m} (c₁ , p₁) (c₂ , p₂) = c₂ ∸ q · c₁ , p
81+
where r = m % suc n; q = n%k≡n[modk] m (suc n) .fst
82+
p = (c₂ ∸ q · c₁) · d ≡⟨ ∸-distribʳ c₂ (q · c₁) d ⟩
83+
c₂ · d ∸ (q · c₁) · d ≡⟨ cong (c₂ · d ∸_) (sym (·-assoc q c₁ d)) ⟩
84+
c₂ · d ∸ q · (c₁ · d) ≡[ i ]⟨ p₂ i ∸ q · (p₁ i) ⟩
85+
m ∸ q · (suc n) ≡⟨ cong (_∸ q · (suc n)) (sym (n%k≡n[modk] m (suc n) .snd)) ⟩
86+
(q · (suc n) + r) ∸ q · (suc n) ≡⟨ cong (_∸ q · (suc n)) (+-comm (q · (suc n)) r) ⟩
87+
(r + q · (suc n)) ∸ q · (suc n) ≡⟨ ∸-cancelʳ r zero (q · (suc n)) ⟩
88+
r ∎
89+
90+
-- The inductive step of the Euclidean algorithm
91+
stepGCD : isGCD (suc n) (m % suc n) d
92+
→ isGCD m (suc n) d
93+
fst (stepGCD ((d∣n , d∣m%n) , gr)) = PropTrunc.map2 lem₁ d∣n d∣m%n , d∣n
94+
snd (stepGCD ((d∣n , d∣m%n) , gr)) d' (d'∣m , d'∣n) = gr d' (d'∣n , PropTrunc.map2 lem₂ d'∣n d'∣m)
95+
96+
-- putting it all together using well-founded induction
97+
98+
euclid< : ∀ m n → n < m → GCD m n
99+
euclid< = WFI.induction <-wellfounded λ {
100+
m rec zero p → m , zeroGCD m ;
101+
m rec (suc n) p → let d , dGCD = rec (suc n) p (m % suc n) (n%sk<sk m n)
102+
in d , stepGCD dGCD }
103+
104+
euclid : ∀ m n → GCD m n
105+
euclid m n with n ≟ m
106+
... | lt p = euclid< m n p
107+
... | gt p = Σ.map-snd symGCD (euclid< n m p)
108+
... | eq p = m , divsGCD (∣-refl (sym p))
109+
110+
isContrGCD : ∀ m n → isContr (GCD m n)
111+
isContrGCD m n = euclid m n , isPropGCD _
112+
113+
-- the gcd operator on ℕ
114+
115+
gcd : ℕ → ℕ → ℕ
116+
gcd m n = euclid m n .fst
117+
118+
gcdIsGCD : ∀ m n → isGCD m n (gcd m n)
119+
gcdIsGCD m n = euclid m n .snd
120+
121+
isGCD→gcd≡ : isGCD m n d → gcd m n ≡ d
122+
isGCD→gcd≡ dGCD = cong fst (isContrGCD _ _ .snd (_ , dGCD))
123+
124+
gcd≡→isGCD : gcd m n ≡ d → isGCD m n d
125+
gcd≡→isGCD p = subst (isGCD _ _) p (gcdIsGCD _ _)
126+
127+
128+
-- multiplicative properties of the gcd
129+
130+
isCD-cancelʳ : ∀ k → isCD (m · suc k) (n · suc k) (d · suc k)
131+
→ isCD m n d
132+
isCD-cancelʳ k (dk∣mk , dk∣nk) = (∣-cancelʳ k dk∣mk , ∣-cancelʳ k dk∣nk)
133+
134+
isCD-multʳ : ∀ k → isCD m n d
135+
→ isCD (m · k) (n · k) (d · k)
136+
isCD-multʳ k (d∣m , d∣n) = (∣-multʳ k d∣m , ∣-multʳ k d∣n)
137+
138+
isGCD-cancelʳ : ∀ k → isGCD (m · suc k) (n · suc k) (d · suc k)
139+
→ isGCD m n d
140+
isGCD-cancelʳ {m} {n} {d} k (dCD , gr) =
141+
isCD-cancelʳ k dCD , λ d' d'CD → ∣-cancelʳ k (gr (d' · suc k) (isCD-multʳ (suc k) d'CD))
142+
143+
gcd-factorʳ : ∀ m n k → gcd (m · k) (n · k) ≡ gcd m n · k
144+
gcd-factorʳ m n zero = (λ i → gcd (0≡m·0 m (~ i)) (0≡m·0 n (~ i))) ∙ 0≡m·0 (gcd m n)
145+
gcd-factorʳ m n (suc k) = sym p ∙ cong (_· suc k) (sym q)
146+
where k∣gcd : suc k ∣ gcd (m · suc k) (n · suc k)
147+
k∣gcd = gcdIsGCD (m · suc k) (n · suc k) .snd (suc k) (∣-right m , ∣-right n)
148+
d' = ∣-untrunc k∣gcd .fst
149+
p : d' · suc k ≡ gcd (m · suc k) (n · suc k)
150+
p = ∣-untrunc k∣gcd .snd
151+
152+
d'GCD : isGCD m n d'
153+
d'GCD = isGCD-cancelʳ _ (subst (isGCD _ _) (sym p) (gcdIsGCD (m · suc k) (n · suc k)))
154+
q : gcd m n ≡ d'
155+
q = isGCD→gcd≡ d'GCD
156+
157+
-- Q: Can this be proved directly? (i.e. without a transport)
158+
isGCD-multʳ : ∀ k → isGCD m n d
159+
→ isGCD (m · k) (n · k) (d · k)
160+
isGCD-multʳ {m} {n} {d} k dGCD = gcd≡→isGCD (gcd-factorʳ m n k ∙ cong (_· k) r)
161+
where r : gcd m n ≡ d
162+
r = isGCD→gcd≡ dGCD
163+
164+
-- Inequality for strict divisibility
165+
166+
stDivIneqGCD : ¬ m ≡ 0 → ¬ m ∣ n → (g : GCD m n) → g .fst < m
167+
stDivIneqGCD p q g = stDivIneq p q (g .snd .fst .fst) (g .snd .fst .snd)

0 commit comments

Comments
 (0)