agda-stdlib-doc 0.14-1 / usr / share / doc / agda-stdlib-doc / html / Data.Nat.GCD.html

This file is indexed.

/usr/share/doc/agda-stdlib-doc/html/Data.Nat.GCD.html is in agda-stdlib-doc 0.14-1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Data.Nat.GCD</title><link rel="stylesheet" href="Agda.css"></head><body><pre><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- Greatest common divisor</a>
<a id="133" class="Comment">------------------------------------------------------------------------</a>

<a id="207" class="Keyword">module</a> <a id="214" href="Data.Nat.GCD.html" class="Module">Data.Nat.GCD</a> <a id="227" class="Keyword">where</a>

<a id="234" class="Keyword">open</a> <a id="239" class="Keyword">import</a> <a id="246" href="Data.Nat.html" class="Module">Data.Nat</a>
<a id="255" class="Keyword">open</a> <a id="260" class="Keyword">import</a> <a id="267" href="Data.Nat.Divisibility.html" class="Module">Data.Nat.Divisibility</a> <a id="289" class="Symbol">as</a> <a id="292" class="Module">Div</a>
<a id="296" class="Keyword">open</a> <a id="301" class="Keyword">import</a> <a id="308" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="324" class="Keyword">private</a> <a id="332" class="Keyword">module</a> <a id="P" href="Data.Nat.GCD.html#P" class="Module">P</a> <a id="341" class="Symbol">=</a> <a id="343" href="Relation.Binary.html#Poset" class="Module">Poset</a> <a id="349" href="Data.Nat.Divisibility.html#poset" class="Function">Div.poset</a>
<a id="359" class="Keyword">open</a> <a id="364" class="Keyword">import</a> <a id="371" href="Data.Product.html" class="Module">Data.Product</a>
<a id="384" class="Keyword">open</a> <a id="389" class="Keyword">import</a> <a id="396" href="Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="434" class="Symbol">as</a> <a id="437" class="Module">PropEq</a> <a id="444" class="Keyword">using</a> <a id="450" class="Symbol">(</a><a id="451" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">_≡_</a><a id="454" class="Symbol">;</a> <a id="456" href="Relation.Binary.PropositionalEquality.Core.html#subst" class="Function">subst</a><a id="461" class="Symbol">)</a>
<a id="463" class="Keyword">open</a> <a id="468" class="Keyword">import</a> <a id="475" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="492" class="Keyword">using</a> <a id="498" class="Symbol">(</a><a id="499" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a><a id="502" class="Symbol">;</a> <a id="504" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a><a id="507" class="Symbol">;</a> <a id="509" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a><a id="511" class="Symbol">)</a>
<a id="513" class="Keyword">open</a> <a id="518" class="Keyword">import</a> <a id="525" href="Induction.html" class="Module">Induction</a>
<a id="535" class="Keyword">open</a> <a id="540" class="Keyword">import</a> <a id="547" href="Induction.Nat.html" class="Module">Induction.Nat</a> <a id="561" class="Keyword">using</a> <a id="567" class="Symbol">(</a><a id="568" href="Induction.Nat.html#%3C%E2%80%B2-Rec" class="Function">&lt;′-Rec</a><a id="574" class="Symbol">;</a> <a id="576" href="Induction.WellFounded.html#1640" class="Function">&lt;′-rec-builder</a><a id="590" class="Symbol">)</a>
<a id="592" class="Keyword">open</a> <a id="597" class="Keyword">import</a> <a id="604" href="Induction.Lexicographic.html" class="Module">Induction.Lexicographic</a>
<a id="628" class="Keyword">open</a> <a id="633" class="Keyword">import</a> <a id="640" href="Function.html" class="Module">Function</a>
<a id="649" class="Keyword">open</a> <a id="654" class="Keyword">import</a> <a id="661" href="Data.Nat.GCD.Lemmas.html" class="Module">Data.Nat.GCD.Lemmas</a>

<a id="682" class="Comment">------------------------------------------------------------------------</a>
<a id="755" class="Comment">-- Greatest common divisor</a>

<a id="783" class="Keyword">module</a> <a id="GCD" href="Data.Nat.GCD.html#GCD" class="Module">GCD</a> <a id="794" class="Keyword">where</a>

  <a id="803" class="Comment">-- Specification of the greatest common divisor (gcd) of two natural</a>
  <a id="874" class="Comment">-- numbers.</a>

  <a id="889" class="Keyword">record</a> <a id="GCD.GCD" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="900" class="Symbol">(</a><a id="901" href="Data.Nat.GCD.html#901" class="Bound">m</a> <a id="903" href="Data.Nat.GCD.html#903" class="Bound">n</a> <a id="905" href="Data.Nat.GCD.html#905" class="Bound">gcd</a> <a id="909" class="Symbol">:</a> <a id="911" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="912" class="Symbol">)</a> <a id="914" class="Symbol">:</a> <a id="916" class="PrimitiveType">Set</a> <a id="920" class="Keyword">where</a>
    <a id="930" class="Keyword">constructor</a> <a id="GCD.GCD.is" href="Data.Nat.GCD.html#GCD.GCD.is" class="InductiveConstructor">is</a>
    <a id="949" class="Keyword">field</a>
      <a id="961" class="Comment">-- The gcd is a common divisor.</a>
      <a id="GCD.GCD.commonDivisor" href="Data.Nat.GCD.html#GCD.GCD.commonDivisor" class="Field">commonDivisor</a> <a id="1013" class="Symbol">:</a> <a id="1015" href="Data.Nat.GCD.html#905" class="Bound">gcd</a> <a id="1019" href="Data.Nat.Divisibility.html#_%E2%88%A3_" class="Datatype Operator">∣</a> <a id="1021" href="Data.Nat.GCD.html#901" class="Bound">m</a> <a id="1023" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="1025" href="Data.Nat.GCD.html#905" class="Bound">gcd</a> <a id="1029" href="Data.Nat.Divisibility.html#_%E2%88%A3_" class="Datatype Operator">∣</a> <a id="1031" href="Data.Nat.GCD.html#903" class="Bound">n</a>

      <a id="1040" class="Comment">-- All common divisors divide the gcd, i.e. the gcd is the</a>
      <a id="1105" class="Comment">-- greatest common divisor according to the partial order _∣_.</a>
      <a id="GCD.GCD.greatest" href="Data.Nat.GCD.html#GCD.GCD.greatest" class="Field">greatest</a> <a id="1183" class="Symbol">:</a> <a id="1185" class="Symbol">∀</a> <a id="1187" class="Symbol">{</a><a id="1188" href="Data.Nat.GCD.html#1188" class="Bound">d</a><a id="1189" class="Symbol">}</a> <a id="1191" class="Symbol">→</a> <a id="1193" href="Data.Nat.GCD.html#1188" class="Bound">d</a> <a id="1195" href="Data.Nat.Divisibility.html#_%E2%88%A3_" class="Datatype Operator">∣</a> <a id="1197" href="Data.Nat.GCD.html#901" class="Bound">m</a> <a id="1199" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="1201" href="Data.Nat.GCD.html#1188" class="Bound">d</a> <a id="1203" href="Data.Nat.Divisibility.html#_%E2%88%A3_" class="Datatype Operator">∣</a> <a id="1205" href="Data.Nat.GCD.html#903" class="Bound">n</a> <a id="1207" class="Symbol">→</a> <a id="1209" href="Data.Nat.GCD.html#1188" class="Bound">d</a> <a id="1211" href="Data.Nat.Divisibility.html#_%E2%88%A3_" class="Datatype Operator">∣</a> <a id="1213" href="Data.Nat.GCD.html#905" class="Bound">gcd</a>

  <a id="1220" class="Keyword">open</a> <a id="1225" href="Data.Nat.GCD.html#GCD" class="Module">GCD</a> <a id="1229" class="Keyword">public</a>

  <a id="1239" class="Comment">-- The gcd is unique.</a>

  <a id="GCD.unique" href="Data.Nat.GCD.html#GCD.unique" class="Function">unique</a> <a id="1271" class="Symbol">:</a> <a id="1273" class="Symbol">∀</a> <a id="1275" class="Symbol">{</a><a id="1276" href="Data.Nat.GCD.html#1276" class="Bound">d₁</a> <a id="1279" href="Data.Nat.GCD.html#1279" class="Bound">d₂</a> <a id="1282" href="Data.Nat.GCD.html#1282" class="Bound">m</a> <a id="1284" href="Data.Nat.GCD.html#1284" class="Bound">n</a><a id="1285" class="Symbol">}</a> <a id="1287" class="Symbol">→</a> <a id="1289" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="1293" href="Data.Nat.GCD.html#1282" class="Bound">m</a> <a id="1295" href="Data.Nat.GCD.html#1284" class="Bound">n</a> <a id="1297" href="Data.Nat.GCD.html#1276" class="Bound">d₁</a> <a id="1300" class="Symbol">→</a> <a id="1302" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="1306" href="Data.Nat.GCD.html#1282" class="Bound">m</a> <a id="1308" href="Data.Nat.GCD.html#1284" class="Bound">n</a> <a id="1310" href="Data.Nat.GCD.html#1279" class="Bound">d₂</a> <a id="1313" class="Symbol">→</a> <a id="1315" href="Data.Nat.GCD.html#1276" class="Bound">d₁</a> <a id="1318" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="1320" href="Data.Nat.GCD.html#1279" class="Bound">d₂</a>
  <a id="1325" href="Data.Nat.GCD.html#GCD.unique" class="Function">unique</a> <a id="1332" href="Data.Nat.GCD.html#1332" class="Bound">d₁</a> <a id="1335" href="Data.Nat.GCD.html#1335" class="Bound">d₂</a> <a id="1338" class="Symbol">=</a> <a id="1340" href="Relation.Binary.html#GCD.P.antisym" class="Function">P.antisym</a> <a id="1350" class="Symbol">(</a><a id="1351" href="Data.Nat.GCD.html#GCD.GCD.greatest" class="Field">GCD.greatest</a> <a id="1364" href="Data.Nat.GCD.html#1335" class="Bound">d₂</a> <a id="1367" class="Symbol">(</a><a id="1368" href="Data.Nat.GCD.html#GCD.GCD.commonDivisor" class="Field">GCD.commonDivisor</a> <a id="1386" href="Data.Nat.GCD.html#1332" class="Bound">d₁</a><a id="1388" class="Symbol">))</a>
                           <a id="1418" class="Symbol">(</a><a id="1419" href="Data.Nat.GCD.html#GCD.GCD.greatest" class="Field">GCD.greatest</a> <a id="1432" href="Data.Nat.GCD.html#1332" class="Bound">d₁</a> <a id="1435" class="Symbol">(</a><a id="1436" href="Data.Nat.GCD.html#GCD.GCD.commonDivisor" class="Field">GCD.commonDivisor</a> <a id="1454" href="Data.Nat.GCD.html#1335" class="Bound">d₂</a><a id="1456" class="Symbol">))</a>

  <a id="1462" class="Comment">-- The gcd relation is &quot;symmetric&quot;.</a>

  <a id="GCD.sym" href="Data.Nat.GCD.html#GCD.sym" class="Function">sym</a> <a id="1505" class="Symbol">:</a> <a id="1507" class="Symbol">∀</a> <a id="1509" class="Symbol">{</a><a id="1510" href="Data.Nat.GCD.html#1510" class="Bound">d</a> <a id="1512" href="Data.Nat.GCD.html#1512" class="Bound">m</a> <a id="1514" href="Data.Nat.GCD.html#1514" class="Bound">n</a><a id="1515" class="Symbol">}</a> <a id="1517" class="Symbol">→</a> <a id="1519" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="1523" href="Data.Nat.GCD.html#1512" class="Bound">m</a> <a id="1525" href="Data.Nat.GCD.html#1514" class="Bound">n</a> <a id="1527" href="Data.Nat.GCD.html#1510" class="Bound">d</a> <a id="1529" class="Symbol">→</a> <a id="1531" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="1535" href="Data.Nat.GCD.html#1514" class="Bound">n</a> <a id="1537" href="Data.Nat.GCD.html#1512" class="Bound">m</a> <a id="1539" href="Data.Nat.GCD.html#1510" class="Bound">d</a>
  <a id="1543" href="Data.Nat.GCD.html#GCD.sym" class="Function">sym</a> <a id="1547" href="Data.Nat.GCD.html#1547" class="Bound">g</a> <a id="1549" class="Symbol">=</a> <a id="1551" href="Data.Nat.GCD.html#GCD.GCD.is" class="InductiveConstructor">is</a> <a id="1554" class="Symbol">(</a><a id="1555" href="Data.Product.html#swap" class="Function">swap</a> <a id="1560" href="Function.html#_%24_" class="Function Operator">$</a> <a id="1562" href="Data.Nat.GCD.html#GCD.GCD.commonDivisor" class="Field">GCD.commonDivisor</a> <a id="1580" href="Data.Nat.GCD.html#1547" class="Bound">g</a><a id="1581" class="Symbol">)</a> <a id="1583" class="Symbol">(</a><a id="1584" href="Data.Nat.GCD.html#GCD.GCD.greatest" class="Field">GCD.greatest</a> <a id="1597" href="Data.Nat.GCD.html#1547" class="Bound">g</a> <a id="1599" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="1601" href="Data.Product.html#swap" class="Function">swap</a><a id="1605" class="Symbol">)</a>

  <a id="1610" class="Comment">-- The gcd relation is &quot;reflexive&quot;.</a>

  <a id="GCD.refl" href="Data.Nat.GCD.html#GCD.refl" class="Function">refl</a> <a id="1654" class="Symbol">:</a> <a id="1656" class="Symbol">∀</a> <a id="1658" class="Symbol">{</a><a id="1659" href="Data.Nat.GCD.html#1659" class="Bound">n</a><a id="1660" class="Symbol">}</a> <a id="1662" class="Symbol">→</a> <a id="1664" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="1668" href="Data.Nat.GCD.html#1659" class="Bound">n</a> <a id="1670" href="Data.Nat.GCD.html#1659" class="Bound">n</a> <a id="1672" href="Data.Nat.GCD.html#1659" class="Bound">n</a>
  <a id="1676" href="Data.Nat.GCD.html#GCD.refl" class="Function">refl</a> <a id="1681" class="Symbol">=</a> <a id="1683" href="Data.Nat.GCD.html#GCD.GCD.is" class="InductiveConstructor">is</a> <a id="1686" class="Symbol">(</a><a id="1687" href="Relation.Binary.html#GCD.P.refl" class="Function">P.refl</a> <a id="1694" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1696" href="Relation.Binary.html#GCD.P.refl" class="Function">P.refl</a><a id="1702" class="Symbol">)</a> <a id="1704" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a>

  <a id="1713" class="Comment">-- The GCD of 0 and n is n.</a>

  <a id="GCD.base" href="Data.Nat.GCD.html#GCD.base" class="Function">base</a> <a id="1749" class="Symbol">:</a> <a id="1751" class="Symbol">∀</a> <a id="1753" class="Symbol">{</a><a id="1754" href="Data.Nat.GCD.html#1754" class="Bound">n</a><a id="1755" class="Symbol">}</a> <a id="1757" class="Symbol">→</a> <a id="1759" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="1763" class="Number">0</a> <a id="1765" href="Data.Nat.GCD.html#1754" class="Bound">n</a> <a id="1767" href="Data.Nat.GCD.html#1754" class="Bound">n</a>
  <a id="1771" href="Data.Nat.GCD.html#GCD.base" class="Function">base</a> <a id="1776" class="Symbol">{</a><a id="1777" href="Data.Nat.GCD.html#1777" class="Bound">n</a><a id="1778" class="Symbol">}</a> <a id="1780" class="Symbol">=</a> <a id="1782" href="Data.Nat.GCD.html#GCD.GCD.is" class="InductiveConstructor">is</a> <a id="1785" class="Symbol">(</a><a id="1786" href="Data.Nat.GCD.html#1777" class="Bound">n</a> <a id="1788" href="Data.Nat.Divisibility.html#_%E2%88%A30" class="Function Operator">∣0</a> <a id="1791" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1793" href="Relation.Binary.html#GCD.P.refl" class="Function">P.refl</a><a id="1799" class="Symbol">)</a> <a id="1801" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a>

  <a id="1810" class="Comment">-- If d is the gcd of n and k, then it is also the gcd of n and</a>
  <a id="1876" class="Comment">-- n + k.</a>

  <a id="GCD.step" href="Data.Nat.GCD.html#GCD.step" class="Function">step</a> <a id="1894" class="Symbol">:</a> <a id="1896" class="Symbol">∀</a> <a id="1898" class="Symbol">{</a><a id="1899" href="Data.Nat.GCD.html#1899" class="Bound">n</a> <a id="1901" href="Data.Nat.GCD.html#1901" class="Bound">k</a> <a id="1903" href="Data.Nat.GCD.html#1903" class="Bound">d</a><a id="1904" class="Symbol">}</a> <a id="1906" class="Symbol">→</a> <a id="1908" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="1912" href="Data.Nat.GCD.html#1899" class="Bound">n</a> <a id="1914" href="Data.Nat.GCD.html#1901" class="Bound">k</a> <a id="1916" href="Data.Nat.GCD.html#1903" class="Bound">d</a> <a id="1918" class="Symbol">→</a> <a id="1920" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="1924" href="Data.Nat.GCD.html#1899" class="Bound">n</a> <a id="1926" class="Symbol">(</a><a id="1927" href="Data.Nat.GCD.html#1899" class="Bound">n</a> <a id="1929" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">+</a> <a id="1931" href="Data.Nat.GCD.html#1901" class="Bound">k</a><a id="1932" class="Symbol">)</a> <a id="1934" href="Data.Nat.GCD.html#1903" class="Bound">d</a>
  <a id="1938" href="Data.Nat.GCD.html#GCD.step" class="Function">step</a> <a id="1943" href="Data.Nat.GCD.html#1943" class="Bound">g</a> <a id="1945" class="Keyword">with</a> <a id="1950" href="Data.Nat.GCD.html#GCD.GCD.commonDivisor" class="Field">GCD.commonDivisor</a> <a id="1968" href="Data.Nat.GCD.html#1943" class="Bound">g</a>
  <a id="1972" href="Data.Nat.GCD.html#GCD.step" class="Function">step</a> <a id="1977" class="Symbol">{</a><a id="1978" href="Data.Nat.GCD.html#1978" class="Bound">n</a><a id="1979" class="Symbol">}</a> <a id="1981" class="Symbol">{</a><a id="1982" href="Data.Nat.GCD.html#1982" class="Bound">k</a><a id="1983" class="Symbol">}</a> <a id="1985" class="Symbol">{</a><a id="1986" href="Data.Nat.GCD.html#1986" class="Bound">d</a><a id="1987" class="Symbol">}</a> <a id="1989" href="Data.Nat.GCD.html#1989" class="Bound">g</a> <a id="1991" class="Symbol">|</a> <a id="1993" class="Symbol">(</a><a id="1994" href="Data.Nat.GCD.html#1994" class="Bound">d₁</a> <a id="1997" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1999" href="Data.Nat.GCD.html#1999" class="Bound">d₂</a><a id="2001" class="Symbol">)</a> <a id="2003" class="Symbol">=</a> <a id="2005" href="Data.Nat.GCD.html#GCD.GCD.is" class="InductiveConstructor">is</a> <a id="2008" class="Symbol">(</a><a id="2009" href="Data.Nat.GCD.html#1994" class="Bound">d₁</a> <a id="2012" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="2014" href="Data.Nat.Divisibility.html#%E2%88%A3m%E2%88%A3n%E2%87%92%E2%88%A3m%2Bn" class="Function">∣m∣n⇒∣m+n</a> <a id="2024" href="Data.Nat.GCD.html#1994" class="Bound">d₁</a> <a id="2027" href="Data.Nat.GCD.html#1999" class="Bound">d₂</a><a id="2029" class="Symbol">)</a> <a id="2031" href="Data.Nat.GCD.html#2055" class="Function">greatest′</a>
    <a id="2045" class="Keyword">where</a>
    <a id="2055" href="Data.Nat.GCD.html#2055" class="Function">greatest′</a> <a id="2065" class="Symbol">:</a> <a id="2067" class="Symbol">∀</a> <a id="2069" class="Symbol">{</a><a id="2070" href="Data.Nat.GCD.html#2070" class="Bound">d′</a><a id="2072" class="Symbol">}</a> <a id="2074" class="Symbol">→</a> <a id="2076" href="Data.Nat.GCD.html#2070" class="Bound">d′</a> <a id="2079" href="Data.Nat.Divisibility.html#_%E2%88%A3_" class="Datatype Operator">∣</a> <a id="2081" href="Data.Nat.GCD.html#1978" class="Bound">n</a> <a id="2083" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="2085" href="Data.Nat.GCD.html#2070" class="Bound">d′</a> <a id="2088" href="Data.Nat.Divisibility.html#_%E2%88%A3_" class="Datatype Operator">∣</a> <a id="2090" href="Data.Nat.GCD.html#1978" class="Bound">n</a> <a id="2092" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">+</a> <a id="2094" href="Data.Nat.GCD.html#1982" class="Bound">k</a> <a id="2096" class="Symbol">→</a> <a id="2098" href="Data.Nat.GCD.html#2070" class="Bound">d′</a> <a id="2101" href="Data.Nat.Divisibility.html#_%E2%88%A3_" class="Datatype Operator">∣</a> <a id="2103" href="Data.Nat.GCD.html#1986" class="Bound">d</a>
    <a id="2109" href="Data.Nat.GCD.html#2055" class="Function">greatest′</a> <a id="2119" class="Symbol">(</a><a id="2120" href="Data.Nat.GCD.html#2120" class="Bound">d₁</a> <a id="2123" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="2125" href="Data.Nat.GCD.html#2125" class="Bound">d₂</a><a id="2127" class="Symbol">)</a> <a id="2129" class="Symbol">=</a> <a id="2131" href="Data.Nat.GCD.html#GCD.GCD.greatest" class="Field">GCD.greatest</a> <a id="2144" href="Data.Nat.GCD.html#1989" class="Bound">g</a> <a id="2146" class="Symbol">(</a><a id="2147" href="Data.Nat.GCD.html#2120" class="Bound">d₁</a> <a id="2150" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="2152" href="Data.Nat.Divisibility.html#%E2%88%A3m%2Bn%7Cm%E2%87%92%7Cn" class="Function">∣m+n|m⇒|n</a> <a id="2162" href="Data.Nat.GCD.html#2125" class="Bound">d₂</a> <a id="2165" href="Data.Nat.GCD.html#2120" class="Bound">d₁</a><a id="2167" class="Symbol">)</a>

<a id="2170" class="Keyword">open</a> <a id="2175" href="Data.Nat.GCD.html#GCD" class="Module">GCD</a> <a id="2179" class="Keyword">public</a> <a id="2186" class="Keyword">using</a> <a id="2192" class="Symbol">(</a><a id="2193" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a><a id="2196" class="Symbol">)</a> <a id="2198" class="Keyword">hiding</a> <a id="2205" class="Symbol">(</a><a id="2206" class="Keyword">module</a> <a id="2213" href="Data.Nat.GCD.html#GCD" class="Module">GCD</a><a id="2216" class="Symbol">)</a>

<a id="2219" class="Comment">------------------------------------------------------------------------</a>
<a id="2292" class="Comment">-- Calculating the gcd</a>

<a id="2316" class="Comment">-- The calculation also proves Bézout&#39;s lemma.</a>

<a id="2364" class="Keyword">module</a> <a id="Bézout" href="Data.Nat.GCD.html#B%C3%A9zout" class="Module">Bézout</a> <a id="2378" class="Keyword">where</a>

  <a id="2387" class="Keyword">module</a> <a id="Identity" href="Data.Nat.GCD.html#Identity" class="Module">Identity</a> <a id="2403" class="Keyword">where</a>

    <a id="2414" class="Comment">-- If m and n have greatest common divisor d, then one of the</a>
    <a id="2480" class="Comment">-- following two equations is satisfied, for some numbers x and y.</a>
    <a id="2551" class="Comment">-- The proof is &quot;lemma&quot; below (Bézout&#39;s lemma).</a>
    <a id="2603" class="Comment">--</a>
    <a id="2610" class="Comment">-- (If this identity was stated using integers instead of natural</a>
    <a id="2680" class="Comment">-- numbers, then it would not be necessary to have two equations.)</a>

    <a id="2752" class="Keyword">data</a> <a id="Bézout.Identity.Identity" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity" class="Datatype">Identity</a> <a id="2766" class="Symbol">(</a><a id="2767" href="Data.Nat.GCD.html#2767" class="Bound">d</a> <a id="2769" href="Data.Nat.GCD.html#2769" class="Bound">m</a> <a id="2771" href="Data.Nat.GCD.html#2771" class="Bound">n</a> <a id="2773" class="Symbol">:</a> <a id="2775" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="2776" class="Symbol">)</a> <a id="2778" class="Symbol">:</a> <a id="2780" class="PrimitiveType">Set</a> <a id="2784" class="Keyword">where</a>
      <a id="Bézout.Identity.Identity.+-" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.%2B-" class="InductiveConstructor">+-</a> <a id="2799" class="Symbol">:</a> <a id="2801" class="Symbol">(</a><a id="2802" href="Data.Nat.GCD.html#2802" class="Bound">x</a> <a id="2804" href="Data.Nat.GCD.html#2804" class="Bound">y</a> <a id="2806" class="Symbol">:</a> <a id="2808" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="2809" class="Symbol">)</a> <a id="2811" class="Symbol">(</a><a id="2812" href="Data.Nat.GCD.html#2812" class="Bound">eq</a> <a id="2815" class="Symbol">:</a> <a id="2817" href="Data.Nat.GCD.html#2767" class="Bound">d</a> <a id="2819" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">+</a> <a id="2821" href="Data.Nat.GCD.html#2804" class="Bound">y</a> <a id="2823" href="Agda.Builtin.Nat.html#_%2A_" class="Primitive Operator">*</a> <a id="2825" href="Data.Nat.GCD.html#2771" class="Bound">n</a> <a id="2827" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="2829" href="Data.Nat.GCD.html#2802" class="Bound">x</a> <a id="2831" href="Agda.Builtin.Nat.html#_%2A_" class="Primitive Operator">*</a> <a id="2833" href="Data.Nat.GCD.html#2769" class="Bound">m</a><a id="2834" class="Symbol">)</a> <a id="2836" class="Symbol">→</a> <a id="2838" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity" class="Datatype">Identity</a> <a id="2847" href="Data.Nat.GCD.html#2767" class="Bound">d</a> <a id="2849" href="Data.Nat.GCD.html#2769" class="Bound">m</a> <a id="2851" href="Data.Nat.GCD.html#2771" class="Bound">n</a>
      <a id="Bézout.Identity.Identity.-+" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a> <a id="2862" class="Symbol">:</a> <a id="2864" class="Symbol">(</a><a id="2865" href="Data.Nat.GCD.html#2865" class="Bound">x</a> <a id="2867" href="Data.Nat.GCD.html#2867" class="Bound">y</a> <a id="2869" class="Symbol">:</a> <a id="2871" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="2872" class="Symbol">)</a> <a id="2874" class="Symbol">(</a><a id="2875" href="Data.Nat.GCD.html#2875" class="Bound">eq</a> <a id="2878" class="Symbol">:</a> <a id="2880" href="Data.Nat.GCD.html#2767" class="Bound">d</a> <a id="2882" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">+</a> <a id="2884" href="Data.Nat.GCD.html#2865" class="Bound">x</a> <a id="2886" href="Agda.Builtin.Nat.html#_%2A_" class="Primitive Operator">*</a> <a id="2888" href="Data.Nat.GCD.html#2769" class="Bound">m</a> <a id="2890" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="2892" href="Data.Nat.GCD.html#2867" class="Bound">y</a> <a id="2894" href="Agda.Builtin.Nat.html#_%2A_" class="Primitive Operator">*</a> <a id="2896" href="Data.Nat.GCD.html#2771" class="Bound">n</a><a id="2897" class="Symbol">)</a> <a id="2899" class="Symbol">→</a> <a id="2901" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity" class="Datatype">Identity</a> <a id="2910" href="Data.Nat.GCD.html#2767" class="Bound">d</a> <a id="2912" href="Data.Nat.GCD.html#2769" class="Bound">m</a> <a id="2914" href="Data.Nat.GCD.html#2771" class="Bound">n</a>

    <a id="2921" class="Comment">-- Various properties about Identity.</a>

    <a id="Bézout.Identity.sym" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.sym" class="Function">sym</a> <a id="2968" class="Symbol">:</a> <a id="2970" class="Symbol">∀</a> <a id="2972" class="Symbol">{</a><a id="2973" href="Data.Nat.GCD.html#2973" class="Bound">d</a><a id="2974" class="Symbol">}</a> <a id="2976" class="Symbol">→</a> <a id="2978" href="Relation.Binary.Core.html#Symmetric" class="Function">Symmetric</a> <a id="2988" class="Symbol">(</a><a id="2989" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity" class="Datatype">Identity</a> <a id="2998" href="Data.Nat.GCD.html#2973" class="Bound">d</a><a id="2999" class="Symbol">)</a>
    <a id="3005" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.sym" class="Function">sym</a> <a id="3009" class="Symbol">(</a><a id="3010" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.%2B-" class="InductiveConstructor">+-</a> <a id="3013" href="Data.Nat.GCD.html#3013" class="Bound">x</a> <a id="3015" href="Data.Nat.GCD.html#3015" class="Bound">y</a> <a id="3017" href="Data.Nat.GCD.html#3017" class="Bound">eq</a><a id="3019" class="Symbol">)</a> <a id="3021" class="Symbol">=</a> <a id="3023" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a> <a id="3026" href="Data.Nat.GCD.html#3015" class="Bound">y</a> <a id="3028" href="Data.Nat.GCD.html#3013" class="Bound">x</a> <a id="3030" href="Data.Nat.GCD.html#3017" class="Bound">eq</a>
    <a id="3037" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.sym" class="Function">sym</a> <a id="3041" class="Symbol">(</a><a id="3042" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a> <a id="3045" href="Data.Nat.GCD.html#3045" class="Bound">x</a> <a id="3047" href="Data.Nat.GCD.html#3047" class="Bound">y</a> <a id="3049" href="Data.Nat.GCD.html#3049" class="Bound">eq</a><a id="3051" class="Symbol">)</a> <a id="3053" class="Symbol">=</a> <a id="3055" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.%2B-" class="InductiveConstructor">+-</a> <a id="3058" href="Data.Nat.GCD.html#3047" class="Bound">y</a> <a id="3060" href="Data.Nat.GCD.html#3045" class="Bound">x</a> <a id="3062" href="Data.Nat.GCD.html#3049" class="Bound">eq</a>

    <a id="Bézout.Identity.refl" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.refl" class="Function">refl</a> <a id="3075" class="Symbol">:</a> <a id="3077" class="Symbol">∀</a> <a id="3079" class="Symbol">{</a><a id="3080" href="Data.Nat.GCD.html#3080" class="Bound">d</a><a id="3081" class="Symbol">}</a> <a id="3083" class="Symbol">→</a> <a id="3085" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity" class="Datatype">Identity</a> <a id="3094" href="Data.Nat.GCD.html#3080" class="Bound">d</a> <a id="3096" href="Data.Nat.GCD.html#3080" class="Bound">d</a> <a id="3098" href="Data.Nat.GCD.html#3080" class="Bound">d</a>
    <a id="3104" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.refl" class="Function">refl</a> <a id="3109" class="Symbol">=</a> <a id="3111" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a> <a id="3114" class="Number">0</a> <a id="3116" class="Number">1</a> <a id="3118" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">PropEq.refl</a>

    <a id="Bézout.Identity.base" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.base" class="Function">base</a> <a id="3140" class="Symbol">:</a> <a id="3142" class="Symbol">∀</a> <a id="3144" class="Symbol">{</a><a id="3145" href="Data.Nat.GCD.html#3145" class="Bound">d</a><a id="3146" class="Symbol">}</a> <a id="3148" class="Symbol">→</a> <a id="3150" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity" class="Datatype">Identity</a> <a id="3159" href="Data.Nat.GCD.html#3145" class="Bound">d</a> <a id="3161" class="Number">0</a> <a id="3163" href="Data.Nat.GCD.html#3145" class="Bound">d</a>
    <a id="3169" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.base" class="Function">base</a> <a id="3174" class="Symbol">=</a> <a id="3176" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a> <a id="3179" class="Number">0</a> <a id="3181" class="Number">1</a> <a id="3183" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">PropEq.refl</a>

    <a id="3200" class="Keyword">private</a>
      <a id="3214" class="Keyword">infixl</a> <a id="3221" class="Number">7</a> <a id="3223" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="Function Operator">_⊕_</a>

      <a id="Bézout.Identity._⊕_" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="Function Operator">_⊕_</a> <a id="3238" class="Symbol">:</a> <a id="3240" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="3242" class="Symbol">→</a> <a id="3244" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="3246" class="Symbol">→</a> <a id="3248" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a>
      <a id="3256" href="Data.Nat.GCD.html#3256" class="Bound">m</a> <a id="3258" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="Function Operator">⊕</a> <a id="3260" href="Data.Nat.GCD.html#3260" class="Bound">n</a> <a id="3262" class="Symbol">=</a> <a id="3264" class="Number">1</a> <a id="3266" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">+</a> <a id="3268" href="Data.Nat.GCD.html#3256" class="Bound">m</a> <a id="3270" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">+</a> <a id="3272" href="Data.Nat.GCD.html#3260" class="Bound">n</a>

    <a id="Bézout.Identity.step" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.step" class="Function">step</a> <a id="3284" class="Symbol">:</a> <a id="3286" class="Symbol">∀</a> <a id="3288" class="Symbol">{</a><a id="3289" href="Data.Nat.GCD.html#3289" class="Bound">d</a> <a id="3291" href="Data.Nat.GCD.html#3291" class="Bound">n</a> <a id="3293" href="Data.Nat.GCD.html#3293" class="Bound">k</a><a id="3294" class="Symbol">}</a> <a id="3296" class="Symbol">→</a> <a id="3298" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity" class="Datatype">Identity</a> <a id="3307" href="Data.Nat.GCD.html#3289" class="Bound">d</a> <a id="3309" href="Data.Nat.GCD.html#3291" class="Bound">n</a> <a id="3311" href="Data.Nat.GCD.html#3293" class="Bound">k</a> <a id="3313" class="Symbol">→</a> <a id="3315" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity" class="Datatype">Identity</a> <a id="3324" href="Data.Nat.GCD.html#3289" class="Bound">d</a> <a id="3326" href="Data.Nat.GCD.html#3291" class="Bound">n</a> <a id="3328" class="Symbol">(</a><a id="3329" href="Data.Nat.GCD.html#3291" class="Bound">n</a> <a id="3331" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">+</a> <a id="3333" href="Data.Nat.GCD.html#3293" class="Bound">k</a><a id="3334" class="Symbol">)</a>
    <a id="3340" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.step" class="Function">step</a> <a id="3345" class="Symbol">{</a><a id="3346" href="Data.Nat.GCD.html#3346" class="Bound">d</a><a id="3347" class="Symbol">}</a>     <a id="3353" class="Symbol">(</a><a id="3354" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.%2B-" class="InductiveConstructor">+-</a>  <a id="3358" href="Data.Nat.GCD.html#3358" class="Bound">x</a>  <a id="3361" href="Data.Nat.GCD.html#3361" class="Bound">y</a>       <a id="3369" href="Data.Nat.GCD.html#3369" class="Bound">eq</a><a id="3371" class="Symbol">)</a> <a id="3373" class="Keyword">with</a> <a id="3378" href="Data.Nat.Base.html#compare" class="Function">compare</a> <a id="3386" href="Data.Nat.GCD.html#3358" class="Bound">x</a> <a id="3388" href="Data.Nat.GCD.html#3361" class="Bound">y</a>
    <a id="3394" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.step" class="Function">step</a> <a id="3399" class="Symbol">{</a><a id="3400" href="Data.Nat.GCD.html#3400" class="Bound">d</a><a id="3401" class="Symbol">}</a>     <a id="3407" class="Symbol">(</a><a id="3408" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.%2B-" class="InductiveConstructor">+-</a> <a id="3411" class="DottedPattern Symbol">.</a><a id="3412" href="Data.Nat.GCD.html#3435" class="DottedPattern Bound">x</a> <a id="3414" class="DottedPattern Symbol">.</a><a id="3415" href="Data.Nat.GCD.html#3435" class="DottedPattern Bound">x</a>       <a id="3423" href="Data.Nat.GCD.html#3423" class="Bound">eq</a><a id="3425" class="Symbol">)</a> <a id="3427" class="Symbol">|</a> <a id="3429" href="Data.Nat.Base.html#Ordering.equal" class="InductiveConstructor">equal</a> <a id="3435" href="Data.Nat.GCD.html#3435" class="Bound">x</a>     <a id="3441" class="Symbol">=</a> <a id="3443" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.%2B-" class="InductiveConstructor">+-</a> <a id="3446" class="Symbol">(</a><a id="3447" class="Number">2</a> <a id="3449" href="Agda.Builtin.Nat.html#_%2A_" class="Primitive Operator">*</a> <a id="3451" href="Data.Nat.GCD.html#3435" class="Bound">x</a><a id="3452" class="Symbol">)</a>     <a id="3458" href="Data.Nat.GCD.html#3435" class="Bound">x</a>       <a id="3466" class="Symbol">(</a><a id="3467" href="Data.Nat.GCD.Lemmas.html#lem%E2%82%82" class="Function">lem₂</a> <a id="3472" href="Data.Nat.GCD.html#3400" class="Bound">d</a> <a id="3474" href="Data.Nat.GCD.html#3435" class="Bound">x</a>   <a id="3478" href="Data.Nat.GCD.html#3423" class="Bound">eq</a><a id="3480" class="Symbol">)</a>
    <a id="3486" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.step" class="Function">step</a> <a id="3491" class="Symbol">{</a><a id="3492" href="Data.Nat.GCD.html#3492" class="Bound">d</a><a id="3493" class="Symbol">}</a>     <a id="3499" class="Symbol">(</a><a id="3500" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.%2B-" class="InductiveConstructor">+-</a> <a id="3503" class="DottedPattern Symbol">.</a><a id="3504" href="Data.Nat.GCD.html#3526" class="DottedPattern Bound">x</a> <a id="3506" class="DottedPattern Symbol">.(</a><a id="3508" href="Data.Nat.GCD.html#3526" class="DottedPattern Bound">x</a> <a id="3510" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="DottedPattern Function Operator">⊕</a> <a id="3512" href="Data.Nat.GCD.html#3528" class="DottedPattern Bound">i</a><a id="3513" class="DottedPattern Symbol">)</a> <a id="3515" href="Data.Nat.GCD.html#3515" class="Bound">eq</a><a id="3517" class="Symbol">)</a> <a id="3519" class="Symbol">|</a> <a id="3521" href="Data.Nat.Base.html#Ordering.less" class="InductiveConstructor">less</a> <a id="3526" href="Data.Nat.GCD.html#3526" class="Bound">x</a> <a id="3528" href="Data.Nat.GCD.html#3528" class="Bound">i</a>    <a id="3533" class="Symbol">=</a> <a id="3535" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.%2B-" class="InductiveConstructor">+-</a> <a id="3538" class="Symbol">(</a><a id="3539" class="Number">2</a> <a id="3541" href="Agda.Builtin.Nat.html#_%2A_" class="Primitive Operator">*</a> <a id="3543" href="Data.Nat.GCD.html#3526" class="Bound">x</a> <a id="3545" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="Function Operator">⊕</a> <a id="3547" href="Data.Nat.GCD.html#3528" class="Bound">i</a><a id="3548" class="Symbol">)</a> <a id="3550" class="Symbol">(</a><a id="3551" href="Data.Nat.GCD.html#3526" class="Bound">x</a> <a id="3553" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="Function Operator">⊕</a> <a id="3555" href="Data.Nat.GCD.html#3528" class="Bound">i</a><a id="3556" class="Symbol">)</a> <a id="3558" class="Symbol">(</a><a id="3559" href="Data.Nat.GCD.Lemmas.html#lem%E2%82%83" class="Function">lem₃</a> <a id="3564" href="Data.Nat.GCD.html#3492" class="Bound">d</a> <a id="3566" href="Data.Nat.GCD.html#3526" class="Bound">x</a>   <a id="3570" href="Data.Nat.GCD.html#3515" class="Bound">eq</a><a id="3572" class="Symbol">)</a>
    <a id="3578" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.step" class="Function">step</a> <a id="3583" class="Symbol">{</a><a id="3584" href="Data.Nat.GCD.html#3584" class="Bound">d</a><a id="3585" class="Symbol">}</a> <a id="3587" class="Symbol">{</a><a id="3588" href="Data.Nat.GCD.html#3588" class="Bound">n</a><a id="3589" class="Symbol">}</a> <a id="3591" class="Symbol">(</a><a id="3592" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.%2B-" class="InductiveConstructor">+-</a> <a id="3595" class="DottedPattern Symbol">.(</a><a id="3597" href="Data.Nat.GCD.html#3621" class="DottedPattern Bound">y</a> <a id="3599" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="DottedPattern Function Operator">⊕</a> <a id="3601" href="Data.Nat.GCD.html#3623" class="DottedPattern Bound">i</a><a id="3602" class="DottedPattern Symbol">)</a> <a id="3604" class="DottedPattern Symbol">.</a><a id="3605" href="Data.Nat.GCD.html#3621" class="DottedPattern Bound">y</a> <a id="3607" href="Data.Nat.GCD.html#3607" class="Bound">eq</a><a id="3609" class="Symbol">)</a> <a id="3611" class="Symbol">|</a> <a id="3613" href="Data.Nat.Base.html#Ordering.greater" class="InductiveConstructor">greater</a> <a id="3621" href="Data.Nat.GCD.html#3621" class="Bound">y</a> <a id="3623" href="Data.Nat.GCD.html#3623" class="Bound">i</a> <a id="3625" class="Symbol">=</a> <a id="3627" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.%2B-" class="InductiveConstructor">+-</a> <a id="3630" class="Symbol">(</a><a id="3631" class="Number">2</a> <a id="3633" href="Agda.Builtin.Nat.html#_%2A_" class="Primitive Operator">*</a> <a id="3635" href="Data.Nat.GCD.html#3621" class="Bound">y</a> <a id="3637" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="Function Operator">⊕</a> <a id="3639" href="Data.Nat.GCD.html#3623" class="Bound">i</a><a id="3640" class="Symbol">)</a> <a id="3642" href="Data.Nat.GCD.html#3621" class="Bound">y</a>       <a id="3650" class="Symbol">(</a><a id="3651" href="Data.Nat.GCD.Lemmas.html#lem%E2%82%84" class="Function">lem₄</a> <a id="3656" href="Data.Nat.GCD.html#3584" class="Bound">d</a> <a id="3658" href="Data.Nat.GCD.html#3621" class="Bound">y</a> <a id="3660" href="Data.Nat.GCD.html#3588" class="Bound">n</a> <a id="3662" href="Data.Nat.GCD.html#3607" class="Bound">eq</a><a id="3664" class="Symbol">)</a>
    <a id="3670" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.step" class="Function">step</a> <a id="3675" class="Symbol">{</a><a id="3676" href="Data.Nat.GCD.html#3676" class="Bound">d</a><a id="3677" class="Symbol">}</a>     <a id="3683" class="Symbol">(</a><a id="3684" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a>  <a id="3688" href="Data.Nat.GCD.html#3688" class="Bound">x</a>  <a id="3691" href="Data.Nat.GCD.html#3691" class="Bound">y</a>       <a id="3699" href="Data.Nat.GCD.html#3699" class="Bound">eq</a><a id="3701" class="Symbol">)</a> <a id="3703" class="Keyword">with</a> <a id="3708" href="Data.Nat.Base.html#compare" class="Function">compare</a> <a id="3716" href="Data.Nat.GCD.html#3688" class="Bound">x</a> <a id="3718" href="Data.Nat.GCD.html#3691" class="Bound">y</a>
    <a id="3724" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.step" class="Function">step</a> <a id="3729" class="Symbol">{</a><a id="3730" href="Data.Nat.GCD.html#3730" class="Bound">d</a><a id="3731" class="Symbol">}</a>     <a id="3737" class="Symbol">(</a><a id="3738" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a> <a id="3741" class="DottedPattern Symbol">.</a><a id="3742" href="Data.Nat.GCD.html#3765" class="DottedPattern Bound">x</a> <a id="3744" class="DottedPattern Symbol">.</a><a id="3745" href="Data.Nat.GCD.html#3765" class="DottedPattern Bound">x</a>       <a id="3753" href="Data.Nat.GCD.html#3753" class="Bound">eq</a><a id="3755" class="Symbol">)</a> <a id="3757" class="Symbol">|</a> <a id="3759" href="Data.Nat.Base.html#Ordering.equal" class="InductiveConstructor">equal</a> <a id="3765" href="Data.Nat.GCD.html#3765" class="Bound">x</a>     <a id="3771" class="Symbol">=</a> <a id="3773" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a> <a id="3776" class="Symbol">(</a><a id="3777" class="Number">2</a> <a id="3779" href="Agda.Builtin.Nat.html#_%2A_" class="Primitive Operator">*</a> <a id="3781" href="Data.Nat.GCD.html#3765" class="Bound">x</a><a id="3782" class="Symbol">)</a>     <a id="3788" href="Data.Nat.GCD.html#3765" class="Bound">x</a>       <a id="3796" class="Symbol">(</a><a id="3797" href="Data.Nat.GCD.Lemmas.html#lem%E2%82%85" class="Function">lem₅</a> <a id="3802" href="Data.Nat.GCD.html#3730" class="Bound">d</a> <a id="3804" href="Data.Nat.GCD.html#3765" class="Bound">x</a>   <a id="3808" href="Data.Nat.GCD.html#3753" class="Bound">eq</a><a id="3810" class="Symbol">)</a>
    <a id="3816" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.step" class="Function">step</a> <a id="3821" class="Symbol">{</a><a id="3822" href="Data.Nat.GCD.html#3822" class="Bound">d</a><a id="3823" class="Symbol">}</a>     <a id="3829" class="Symbol">(</a><a id="3830" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a> <a id="3833" class="DottedPattern Symbol">.</a><a id="3834" href="Data.Nat.GCD.html#3856" class="DottedPattern Bound">x</a> <a id="3836" class="DottedPattern Symbol">.(</a><a id="3838" href="Data.Nat.GCD.html#3856" class="DottedPattern Bound">x</a> <a id="3840" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="DottedPattern Function Operator">⊕</a> <a id="3842" href="Data.Nat.GCD.html#3858" class="DottedPattern Bound">i</a><a id="3843" class="DottedPattern Symbol">)</a> <a id="3845" href="Data.Nat.GCD.html#3845" class="Bound">eq</a><a id="3847" class="Symbol">)</a> <a id="3849" class="Symbol">|</a> <a id="3851" href="Data.Nat.Base.html#Ordering.less" class="InductiveConstructor">less</a> <a id="3856" href="Data.Nat.GCD.html#3856" class="Bound">x</a> <a id="3858" href="Data.Nat.GCD.html#3858" class="Bound">i</a>    <a id="3863" class="Symbol">=</a> <a id="3865" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a> <a id="3868" class="Symbol">(</a><a id="3869" class="Number">2</a> <a id="3871" href="Agda.Builtin.Nat.html#_%2A_" class="Primitive Operator">*</a> <a id="3873" href="Data.Nat.GCD.html#3856" class="Bound">x</a> <a id="3875" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="Function Operator">⊕</a> <a id="3877" href="Data.Nat.GCD.html#3858" class="Bound">i</a><a id="3878" class="Symbol">)</a> <a id="3880" class="Symbol">(</a><a id="3881" href="Data.Nat.GCD.html#3856" class="Bound">x</a> <a id="3883" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="Function Operator">⊕</a> <a id="3885" href="Data.Nat.GCD.html#3858" class="Bound">i</a><a id="3886" class="Symbol">)</a> <a id="3888" class="Symbol">(</a><a id="3889" href="Data.Nat.GCD.Lemmas.html#lem%E2%82%86" class="Function">lem₆</a> <a id="3894" href="Data.Nat.GCD.html#3822" class="Bound">d</a> <a id="3896" href="Data.Nat.GCD.html#3856" class="Bound">x</a>   <a id="3900" href="Data.Nat.GCD.html#3845" class="Bound">eq</a><a id="3902" class="Symbol">)</a>
    <a id="3908" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.step" class="Function">step</a> <a id="3913" class="Symbol">{</a><a id="3914" href="Data.Nat.GCD.html#3914" class="Bound">d</a><a id="3915" class="Symbol">}</a> <a id="3917" class="Symbol">{</a><a id="3918" href="Data.Nat.GCD.html#3918" class="Bound">n</a><a id="3919" class="Symbol">}</a> <a id="3921" class="Symbol">(</a><a id="3922" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a> <a id="3925" class="DottedPattern Symbol">.(</a><a id="3927" href="Data.Nat.GCD.html#3951" class="DottedPattern Bound">y</a> <a id="3929" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="DottedPattern Function Operator">⊕</a> <a id="3931" href="Data.Nat.GCD.html#3953" class="DottedPattern Bound">i</a><a id="3932" class="DottedPattern Symbol">)</a> <a id="3934" class="DottedPattern Symbol">.</a><a id="3935" href="Data.Nat.GCD.html#3951" class="DottedPattern Bound">y</a> <a id="3937" href="Data.Nat.GCD.html#3937" class="Bound">eq</a><a id="3939" class="Symbol">)</a> <a id="3941" class="Symbol">|</a> <a id="3943" href="Data.Nat.Base.html#Ordering.greater" class="InductiveConstructor">greater</a> <a id="3951" href="Data.Nat.GCD.html#3951" class="Bound">y</a> <a id="3953" href="Data.Nat.GCD.html#3953" class="Bound">i</a> <a id="3955" class="Symbol">=</a> <a id="3957" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a> <a id="3960" class="Symbol">(</a><a id="3961" class="Number">2</a> <a id="3963" href="Agda.Builtin.Nat.html#_%2A_" class="Primitive Operator">*</a> <a id="3965" href="Data.Nat.GCD.html#3951" class="Bound">y</a> <a id="3967" href="Data.Nat.GCD.html#B%C3%A9zout.Identity._%E2%8A%95_" class="Function Operator">⊕</a> <a id="3969" href="Data.Nat.GCD.html#3953" class="Bound">i</a><a id="3970" class="Symbol">)</a> <a id="3972" href="Data.Nat.GCD.html#3951" class="Bound">y</a>       <a id="3980" class="Symbol">(</a><a id="3981" href="Data.Nat.GCD.Lemmas.html#lem%E2%82%87" class="Function">lem₇</a> <a id="3986" href="Data.Nat.GCD.html#3914" class="Bound">d</a> <a id="3988" href="Data.Nat.GCD.html#3951" class="Bound">y</a> <a id="3990" href="Data.Nat.GCD.html#3918" class="Bound">n</a> <a id="3992" href="Data.Nat.GCD.html#3937" class="Bound">eq</a><a id="3994" class="Symbol">)</a>

  <a id="3999" class="Keyword">open</a> <a id="4004" href="Data.Nat.GCD.html#Identity" class="Module">Identity</a> <a id="4013" class="Keyword">public</a> <a id="4020" class="Keyword">using</a> <a id="4026" class="Symbol">(</a><a id="4027" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity" class="Datatype">Identity</a><a id="4035" class="Symbol">;</a> <a id="4037" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.%2B-" class="InductiveConstructor">+-</a><a id="4039" class="Symbol">;</a> <a id="4041" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity.-%2B" class="InductiveConstructor">-+</a><a id="4043" class="Symbol">)</a> <a id="4045" class="Keyword">hiding</a> <a id="4052" class="Symbol">(</a><a id="4053" class="Keyword">module</a> <a id="4060" href="Data.Nat.GCD.html#Identity" class="Module">Identity</a><a id="4068" class="Symbol">)</a>

  <a id="4073" class="Keyword">module</a> <a id="Lemma" href="Data.Nat.GCD.html#Lemma" class="Module">Lemma</a> <a id="4086" class="Keyword">where</a>

    <a id="4097" class="Comment">-- This type packs up the gcd, the proof that it is a gcd, and the</a>
    <a id="4168" class="Comment">-- proof that it satisfies Bézout&#39;s identity.</a>

    <a id="4219" class="Keyword">data</a> <a id="Bézout.Lemma.Lemma" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a> <a id="4230" class="Symbol">(</a><a id="4231" href="Data.Nat.GCD.html#4231" class="Bound">m</a> <a id="4233" href="Data.Nat.GCD.html#4233" class="Bound">n</a> <a id="4235" class="Symbol">:</a> <a id="4237" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="4238" class="Symbol">)</a> <a id="4240" class="Symbol">:</a> <a id="4242" class="PrimitiveType">Set</a> <a id="4246" class="Keyword">where</a>
      <a id="Bézout.Lemma.Lemma.result" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma.result" class="InductiveConstructor">result</a> <a id="4265" class="Symbol">:</a> <a id="4267" class="Symbol">(</a><a id="4268" href="Data.Nat.GCD.html#4268" class="Bound">d</a> <a id="4270" class="Symbol">:</a> <a id="4272" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="4273" class="Symbol">)</a> <a id="4275" class="Symbol">(</a><a id="4276" href="Data.Nat.GCD.html#4276" class="Bound">g</a> <a id="4278" class="Symbol">:</a> <a id="4280" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="4284" href="Data.Nat.GCD.html#4231" class="Bound">m</a> <a id="4286" href="Data.Nat.GCD.html#4233" class="Bound">n</a> <a id="4288" href="Data.Nat.GCD.html#4268" class="Bound">d</a><a id="4289" class="Symbol">)</a> <a id="4291" class="Symbol">(</a><a id="4292" href="Data.Nat.GCD.html#4292" class="Bound">b</a> <a id="4294" class="Symbol">:</a> <a id="4296" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity" class="Datatype">Identity</a> <a id="4305" href="Data.Nat.GCD.html#4268" class="Bound">d</a> <a id="4307" href="Data.Nat.GCD.html#4231" class="Bound">m</a> <a id="4309" href="Data.Nat.GCD.html#4233" class="Bound">n</a><a id="4310" class="Symbol">)</a> <a id="4312" class="Symbol">→</a> <a id="4314" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a> <a id="4320" href="Data.Nat.GCD.html#4231" class="Bound">m</a> <a id="4322" href="Data.Nat.GCD.html#4233" class="Bound">n</a>

    <a id="4329" class="Comment">-- Various properties about Lemma.</a>

    <a id="Bézout.Lemma.sym" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.sym" class="Function">sym</a> <a id="4373" class="Symbol">:</a> <a id="4375" href="Relation.Binary.Core.html#Symmetric" class="Function">Symmetric</a> <a id="4385" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a>
    <a id="4395" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.sym" class="Function">sym</a> <a id="4399" class="Symbol">(</a><a id="4400" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma.result" class="InductiveConstructor">result</a> <a id="4407" href="Data.Nat.GCD.html#4407" class="Bound">d</a> <a id="4409" href="Data.Nat.GCD.html#4409" class="Bound">g</a> <a id="4411" href="Data.Nat.GCD.html#4411" class="Bound">b</a><a id="4412" class="Symbol">)</a> <a id="4414" class="Symbol">=</a> <a id="4416" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma.result" class="InductiveConstructor">result</a> <a id="4423" href="Data.Nat.GCD.html#4407" class="Bound">d</a> <a id="4425" class="Symbol">(</a><a id="4426" href="Data.Nat.GCD.html#GCD.sym" class="Function">GCD.sym</a> <a id="4434" href="Data.Nat.GCD.html#4409" class="Bound">g</a><a id="4435" class="Symbol">)</a> <a id="4437" class="Symbol">(</a><a id="4438" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.sym" class="Function">Identity.sym</a> <a id="4451" href="Data.Nat.GCD.html#4411" class="Bound">b</a><a id="4452" class="Symbol">)</a>

    <a id="Bézout.Lemma.base" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.base" class="Function">base</a> <a id="4464" class="Symbol">:</a> <a id="4466" class="Symbol">∀</a> <a id="4468" href="Data.Nat.GCD.html#4468" class="Bound">d</a> <a id="4470" class="Symbol">→</a> <a id="4472" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a> <a id="4478" class="Number">0</a> <a id="4480" href="Data.Nat.GCD.html#4468" class="Bound">d</a>
    <a id="4486" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.base" class="Function">base</a> <a id="4491" href="Data.Nat.GCD.html#4491" class="Bound">d</a> <a id="4493" class="Symbol">=</a> <a id="4495" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma.result" class="InductiveConstructor">result</a> <a id="4502" href="Data.Nat.GCD.html#4491" class="Bound">d</a> <a id="4504" href="Data.Nat.GCD.html#GCD.base" class="Function">GCD.base</a> <a id="4513" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.base" class="Function">Identity.base</a>

    <a id="Bézout.Lemma.refl" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.refl" class="Function">refl</a> <a id="4537" class="Symbol">:</a> <a id="4539" class="Symbol">∀</a> <a id="4541" href="Data.Nat.GCD.html#4541" class="Bound">d</a> <a id="4543" class="Symbol">→</a> <a id="4545" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a> <a id="4551" href="Data.Nat.GCD.html#4541" class="Bound">d</a> <a id="4553" href="Data.Nat.GCD.html#4541" class="Bound">d</a>
    <a id="4559" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.refl" class="Function">refl</a> <a id="4564" href="Data.Nat.GCD.html#4564" class="Bound">d</a> <a id="4566" class="Symbol">=</a> <a id="4568" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma.result" class="InductiveConstructor">result</a> <a id="4575" href="Data.Nat.GCD.html#4564" class="Bound">d</a> <a id="4577" href="Data.Nat.GCD.html#GCD.refl" class="Function">GCD.refl</a> <a id="4586" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.refl" class="Function">Identity.refl</a>

    <a id="Bézout.Lemma.stepˡ" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.step%CB%A1" class="Function">stepˡ</a> <a id="4611" class="Symbol">:</a> <a id="4613" class="Symbol">∀</a> <a id="4615" class="Symbol">{</a><a id="4616" href="Data.Nat.GCD.html#4616" class="Bound">n</a> <a id="4618" href="Data.Nat.GCD.html#4618" class="Bound">k</a><a id="4619" class="Symbol">}</a> <a id="4621" class="Symbol">→</a> <a id="4623" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a> <a id="4629" href="Data.Nat.GCD.html#4616" class="Bound">n</a> <a id="4631" class="Symbol">(</a><a id="4632" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="4636" href="Data.Nat.GCD.html#4618" class="Bound">k</a><a id="4637" class="Symbol">)</a> <a id="4639" class="Symbol">→</a> <a id="4641" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a> <a id="4647" href="Data.Nat.GCD.html#4616" class="Bound">n</a> <a id="4649" class="Symbol">(</a><a id="4650" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="4654" class="Symbol">(</a><a id="4655" href="Data.Nat.GCD.html#4616" class="Bound">n</a> <a id="4657" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">+</a> <a id="4659" href="Data.Nat.GCD.html#4618" class="Bound">k</a><a id="4660" class="Symbol">))</a>
    <a id="4667" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.step%CB%A1" class="Function">stepˡ</a> <a id="4673" class="Symbol">{</a><a id="4674" href="Data.Nat.GCD.html#4674" class="Bound">n</a><a id="4675" class="Symbol">}</a> <a id="4677" class="Symbol">{</a><a id="4678" href="Data.Nat.GCD.html#4678" class="Bound">k</a><a id="4679" class="Symbol">}</a> <a id="4681" class="Symbol">(</a><a id="4682" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma.result" class="InductiveConstructor">result</a> <a id="4689" href="Data.Nat.GCD.html#4689" class="Bound">d</a> <a id="4691" href="Data.Nat.GCD.html#4691" class="Bound">g</a> <a id="4693" href="Data.Nat.GCD.html#4693" class="Bound">b</a><a id="4694" class="Symbol">)</a> <a id="4696" class="Symbol">=</a>
      <a id="4704" href="Relation.Binary.PropositionalEquality.Core.html#subst" class="Function">PropEq.subst</a> <a id="4717" class="Symbol">(</a><a id="4718" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a> <a id="4724" href="Data.Nat.GCD.html#4674" class="Bound">n</a><a id="4725" class="Symbol">)</a> <a id="4727" class="Symbol">(</a><a id="4728" href="Data.Nat.GCD.Lemmas.html#lem%E2%82%80" class="Function">lem₀</a> <a id="4733" href="Data.Nat.GCD.html#4674" class="Bound">n</a> <a id="4735" href="Data.Nat.GCD.html#4678" class="Bound">k</a><a id="4736" class="Symbol">)</a> <a id="4738" href="Function.html#_%24_" class="Function Operator">$</a>
        <a id="4748" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma.result" class="InductiveConstructor">result</a> <a id="4755" href="Data.Nat.GCD.html#4689" class="Bound">d</a> <a id="4757" class="Symbol">(</a><a id="4758" href="Data.Nat.GCD.html#GCD.step" class="Function">GCD.step</a> <a id="4767" href="Data.Nat.GCD.html#4691" class="Bound">g</a><a id="4768" class="Symbol">)</a> <a id="4770" class="Symbol">(</a><a id="4771" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.step" class="Function">Identity.step</a> <a id="4785" href="Data.Nat.GCD.html#4693" class="Bound">b</a><a id="4786" class="Symbol">)</a>

    <a id="Bézout.Lemma.stepʳ" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.step%CA%B3" class="Function">stepʳ</a> <a id="4799" class="Symbol">:</a> <a id="4801" class="Symbol">∀</a> <a id="4803" class="Symbol">{</a><a id="4804" href="Data.Nat.GCD.html#4804" class="Bound">n</a> <a id="4806" href="Data.Nat.GCD.html#4806" class="Bound">k</a><a id="4807" class="Symbol">}</a> <a id="4809" class="Symbol">→</a> <a id="4811" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a> <a id="4817" class="Symbol">(</a><a id="4818" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="4822" href="Data.Nat.GCD.html#4806" class="Bound">k</a><a id="4823" class="Symbol">)</a> <a id="4825" href="Data.Nat.GCD.html#4804" class="Bound">n</a> <a id="4827" class="Symbol">→</a> <a id="4829" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a> <a id="4835" class="Symbol">(</a><a id="4836" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="4840" class="Symbol">(</a><a id="4841" href="Data.Nat.GCD.html#4804" class="Bound">n</a> <a id="4843" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">+</a> <a id="4845" href="Data.Nat.GCD.html#4806" class="Bound">k</a><a id="4846" class="Symbol">))</a> <a id="4849" href="Data.Nat.GCD.html#4804" class="Bound">n</a>
    <a id="4855" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.step%CA%B3" class="Function">stepʳ</a> <a id="4861" class="Symbol">=</a> <a id="4863" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.sym" class="Function">sym</a> <a id="4867" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="4869" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.step%CB%A1" class="Function">stepˡ</a> <a id="4875" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="4877" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.sym" class="Function">sym</a>

  <a id="4884" class="Keyword">open</a> <a id="4889" href="Data.Nat.GCD.html#Lemma" class="Module">Lemma</a> <a id="4895" class="Keyword">public</a> <a id="4902" class="Keyword">using</a> <a id="4908" class="Symbol">(</a><a id="4909" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a><a id="4914" class="Symbol">;</a> <a id="4916" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma.result" class="InductiveConstructor">result</a><a id="4922" class="Symbol">)</a> <a id="4924" class="Keyword">hiding</a> <a id="4931" class="Symbol">(</a><a id="4932" class="Keyword">module</a> <a id="4939" href="Data.Nat.GCD.html#Lemma" class="Module">Lemma</a><a id="4944" class="Symbol">)</a>

  <a id="4949" class="Comment">-- Bézout&#39;s lemma proved using some variant of the extended</a>
  <a id="5011" class="Comment">-- Euclidean algorithm.</a>

  <a id="Bézout.lemma" href="Data.Nat.GCD.html#B%C3%A9zout.lemma" class="Function">lemma</a> <a id="5044" class="Symbol">:</a> <a id="5046" class="Symbol">(</a><a id="5047" href="Data.Nat.GCD.html#5047" class="Bound">m</a> <a id="5049" href="Data.Nat.GCD.html#5049" class="Bound">n</a> <a id="5051" class="Symbol">:</a> <a id="5053" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="5054" class="Symbol">)</a> <a id="5056" class="Symbol">→</a> <a id="5058" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a> <a id="5064" href="Data.Nat.GCD.html#5047" class="Bound">m</a> <a id="5066" href="Data.Nat.GCD.html#5049" class="Bound">n</a>
  <a id="5070" href="Data.Nat.GCD.html#B%C3%A9zout.lemma" class="Function">lemma</a> <a id="5076" href="Data.Nat.GCD.html#5076" class="Bound">m</a> <a id="5078" href="Data.Nat.GCD.html#5078" class="Bound">n</a> <a id="5080" class="Symbol">=</a> <a id="5082" href="Induction.html#build" class="Function">build</a> <a id="5088" href="Induction.Lexicographic.html#%5B_%E2%8A%97_%5D" class="Function Operator">[</a> <a id="5090" href="Induction.WellFounded.html#1640" class="Function">&lt;′-rec-builder</a> <a id="5105" href="Induction.Lexicographic.html#%5B_%E2%8A%97_%5D" class="Function Operator">⊗</a> <a id="5107" href="Induction.WellFounded.html#1640" class="Function">&lt;′-rec-builder</a> <a id="5122" href="Induction.Lexicographic.html#%5B_%E2%8A%97_%5D" class="Function Operator">]</a> <a id="5124" href="Data.Nat.GCD.html#5152" class="Function">P</a> <a id="5126" href="Data.Nat.GCD.html#5199" class="Function">gcd</a> <a id="5130" class="Symbol">(</a><a id="5131" href="Data.Nat.GCD.html#5076" class="Bound">m</a> <a id="5133" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5135" href="Data.Nat.GCD.html#5078" class="Bound">n</a><a id="5136" class="Symbol">)</a>
    <a id="5142" class="Keyword">where</a>
    <a id="5152" href="Data.Nat.GCD.html#5152" class="Function">P</a> <a id="5154" class="Symbol">:</a> <a id="5156" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="5158" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="5160" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="5162" class="Symbol">→</a> <a id="5164" class="PrimitiveType">Set</a>
    <a id="5172" href="Data.Nat.GCD.html#5152" class="Function">P</a> <a id="5174" class="Symbol">(</a><a id="5175" href="Data.Nat.GCD.html#5175" class="Bound">m</a> <a id="5177" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5179" href="Data.Nat.GCD.html#5179" class="Bound">n</a><a id="5180" class="Symbol">)</a> <a id="5182" class="Symbol">=</a> <a id="5184" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma" class="Datatype">Lemma</a> <a id="5190" href="Data.Nat.GCD.html#5175" class="Bound">m</a> <a id="5192" href="Data.Nat.GCD.html#5179" class="Bound">n</a>

    <a id="5199" href="Data.Nat.GCD.html#5199" class="Function">gcd</a> <a id="5203" class="Symbol">:</a> <a id="5205" class="Symbol">∀</a> <a id="5207" href="Data.Nat.GCD.html#5207" class="Bound">p</a> <a id="5209" class="Symbol">→</a> <a id="5211" class="Symbol">(</a><a id="5212" href="Induction.Nat.html#%3C%E2%80%B2-Rec" class="Function">&lt;′-Rec</a> <a id="5219" href="Induction.Lexicographic.html#_%E2%8A%97_" class="Function Operator">⊗</a> <a id="5221" href="Induction.Nat.html#%3C%E2%80%B2-Rec" class="Function">&lt;′-Rec</a><a id="5227" class="Symbol">)</a> <a id="5229" href="Data.Nat.GCD.html#5152" class="Function">P</a> <a id="5231" href="Data.Nat.GCD.html#5207" class="Bound">p</a> <a id="5233" class="Symbol">→</a> <a id="5235" href="Data.Nat.GCD.html#5152" class="Function">P</a> <a id="5237" href="Data.Nat.GCD.html#5207" class="Bound">p</a>
    <a id="5243" href="Data.Nat.GCD.html#5199" class="Function">gcd</a> <a id="5247" class="Symbol">(</a><a id="5248" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a>  <a id="5254" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5256" href="Data.Nat.GCD.html#5256" class="Bound">n</a>                 <a id="5274" class="Symbol">)</a> <a id="5276" href="Data.Nat.GCD.html#5276" class="Bound">rec</a> <a id="5280" class="Symbol">=</a> <a id="5282" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.base" class="Function">Lemma.base</a> <a id="5293" href="Data.Nat.GCD.html#5256" class="Bound">n</a>
    <a id="5299" href="Data.Nat.GCD.html#5199" class="Function">gcd</a> <a id="5303" class="Symbol">(</a><a id="5304" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5308" href="Data.Nat.GCD.html#5308" class="Bound">m</a> <a id="5310" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5312" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a>              <a id="5330" class="Symbol">)</a> <a id="5332" href="Data.Nat.GCD.html#5332" class="Bound">rec</a> <a id="5336" class="Symbol">=</a> <a id="5338" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.sym" class="Function">Lemma.sym</a> <a id="5348" class="Symbol">(</a><a id="5349" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.base" class="Function">Lemma.base</a> <a id="5360" class="Symbol">(</a><a id="5361" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5365" href="Data.Nat.GCD.html#5308" class="Bound">m</a><a id="5366" class="Symbol">))</a>
    <a id="5373" href="Data.Nat.GCD.html#5199" class="Function">gcd</a> <a id="5377" class="Symbol">(</a><a id="5378" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5382" href="Data.Nat.GCD.html#5382" class="Bound">m</a> <a id="5384" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5386" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5390" href="Data.Nat.GCD.html#5390" class="Bound">n</a>             <a id="5404" class="Symbol">)</a> <a id="5406" href="Data.Nat.GCD.html#5406" class="Bound">rec</a> <a id="5410" class="Keyword">with</a> <a id="5415" href="Data.Nat.Base.html#compare" class="Function">compare</a> <a id="5423" href="Data.Nat.GCD.html#5382" class="Bound">m</a> <a id="5425" href="Data.Nat.GCD.html#5390" class="Bound">n</a>
    <a id="5431" href="Data.Nat.GCD.html#5199" class="Function">gcd</a> <a id="5435" class="Symbol">(</a><a id="5436" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5440" href="Data.Nat.GCD.html#5440" class="Bound">m</a> <a id="5442" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5444" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5448" class="DottedPattern Symbol">.</a><a id="5449" href="Data.Nat.GCD.html#5440" class="DottedPattern Bound">m</a>            <a id="5462" class="Symbol">)</a> <a id="5464" href="Data.Nat.GCD.html#5464" class="Bound">rec</a> <a id="5468" class="Symbol">|</a> <a id="5470" href="Data.Nat.Base.html#Ordering.equal" class="InductiveConstructor">equal</a> <a id="5476" class="DottedPattern Symbol">.</a><a id="5477" href="Data.Nat.GCD.html#5440" class="DottedPattern Bound">m</a>     <a id="5483" class="Symbol">=</a> <a id="5485" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.refl" class="Function">Lemma.refl</a> <a id="5496" class="Symbol">(</a><a id="5497" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5501" href="Data.Nat.GCD.html#5440" class="Bound">m</a><a id="5502" class="Symbol">)</a>
    <a id="5508" href="Data.Nat.GCD.html#5199" class="Function">gcd</a> <a id="5512" class="Symbol">(</a><a id="5513" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5517" href="Data.Nat.GCD.html#5517" class="Bound">m</a> <a id="5519" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5521" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5525" class="DottedPattern Symbol">.(</a><a id="5527" href="Agda.Builtin.Nat.html#Nat.suc" class="DottedPattern InductiveConstructor">suc</a> <a id="5531" class="DottedPattern Symbol">(</a><a id="5532" href="Data.Nat.GCD.html#5517" class="DottedPattern Bound">m</a> <a id="5534" href="Agda.Builtin.Nat.html#_%2B_" class="DottedPattern Primitive Operator">+</a> <a id="5536" href="Data.Nat.GCD.html#5555" class="DottedPattern Bound">k</a><a id="5537" class="DottedPattern Symbol">))</a><a id="5539" class="Symbol">)</a> <a id="5541" href="Data.Nat.GCD.html#5541" class="Bound">rec</a> <a id="5545" class="Symbol">|</a> <a id="5547" href="Data.Nat.Base.html#Ordering.less" class="InductiveConstructor">less</a> <a id="5552" class="DottedPattern Symbol">.</a><a id="5553" href="Data.Nat.GCD.html#5517" class="DottedPattern Bound">m</a> <a id="5555" href="Data.Nat.GCD.html#5555" class="Bound">k</a>    <a id="5560" class="Symbol">=</a>
                      <a id="5584" class="Comment">-- &quot;gcd (suc m) (suc k)&quot;</a>
      <a id="5615" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.step%CB%A1" class="Function">Lemma.stepˡ</a> <a id="5627" href="Function.html#_%24_" class="Function Operator">$</a> <a id="5629" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a> <a id="5635" href="Data.Nat.GCD.html#5541" class="Bound">rec</a> <a id="5639" class="Symbol">(</a><a id="5640" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5644" href="Data.Nat.GCD.html#5555" class="Bound">k</a><a id="5645" class="Symbol">)</a> <a id="5647" class="Symbol">(</a><a id="5648" href="Data.Nat.GCD.Lemmas.html#lem%E2%82%81" class="Function">lem₁</a> <a id="5653" href="Data.Nat.GCD.html#5555" class="Bound">k</a> <a id="5655" href="Data.Nat.GCD.html#5517" class="Bound">m</a><a id="5656" class="Symbol">)</a>
    <a id="5662" href="Data.Nat.GCD.html#5199" class="Function">gcd</a> <a id="5666" class="Symbol">(</a><a id="5667" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5671" class="DottedPattern Symbol">.(</a><a id="5673" href="Agda.Builtin.Nat.html#Nat.suc" class="DottedPattern InductiveConstructor">suc</a> <a id="5677" class="DottedPattern Symbol">(</a><a id="5678" href="Data.Nat.GCD.html#5692" class="DottedPattern Bound">n</a> <a id="5680" href="Agda.Builtin.Nat.html#_%2B_" class="DottedPattern Primitive Operator">+</a> <a id="5682" href="Data.Nat.GCD.html#5712" class="DottedPattern Bound">k</a><a id="5683" class="DottedPattern Symbol">))</a> <a id="5686" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5688" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5692" href="Data.Nat.GCD.html#5692" class="Bound">n</a><a id="5693" class="Symbol">)</a> <a id="5695" href="Data.Nat.GCD.html#5695" class="Bound">rec</a> <a id="5699" class="Symbol">|</a> <a id="5701" href="Data.Nat.Base.html#Ordering.greater" class="InductiveConstructor">greater</a> <a id="5709" class="DottedPattern Symbol">.</a><a id="5710" href="Data.Nat.GCD.html#5692" class="DottedPattern Bound">n</a> <a id="5712" href="Data.Nat.GCD.html#5712" class="Bound">k</a> <a id="5714" class="Symbol">=</a>
                      <a id="5738" class="Comment">-- &quot;gcd (suc k) (suc n)&quot;</a>
      <a id="5769" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.step%CA%B3" class="Function">Lemma.stepʳ</a> <a id="5781" href="Function.html#_%24_" class="Function Operator">$</a> <a id="5783" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a> <a id="5789" href="Data.Nat.GCD.html#5695" class="Bound">rec</a> <a id="5793" class="Symbol">(</a><a id="5794" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5798" href="Data.Nat.GCD.html#5712" class="Bound">k</a><a id="5799" class="Symbol">)</a> <a id="5801" class="Symbol">(</a><a id="5802" href="Data.Nat.GCD.Lemmas.html#lem%E2%82%81" class="Function">lem₁</a> <a id="5807" href="Data.Nat.GCD.html#5712" class="Bound">k</a> <a id="5809" href="Data.Nat.GCD.html#5692" class="Bound">n</a><a id="5810" class="Symbol">)</a> <a id="5812" class="Symbol">(</a><a id="5813" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="5817" href="Data.Nat.GCD.html#5692" class="Bound">n</a><a id="5818" class="Symbol">)</a>

  <a id="5823" class="Comment">-- Bézout&#39;s identity can be recovered from the GCD.</a>

  <a id="Bézout.identity" href="Data.Nat.GCD.html#B%C3%A9zout.identity" class="Function">identity</a> <a id="5887" class="Symbol">:</a> <a id="5889" class="Symbol">∀</a> <a id="5891" class="Symbol">{</a><a id="5892" href="Data.Nat.GCD.html#5892" class="Bound">m</a> <a id="5894" href="Data.Nat.GCD.html#5894" class="Bound">n</a> <a id="5896" href="Data.Nat.GCD.html#5896" class="Bound">d</a><a id="5897" class="Symbol">}</a> <a id="5899" class="Symbol">→</a> <a id="5901" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="5905" href="Data.Nat.GCD.html#5892" class="Bound">m</a> <a id="5907" href="Data.Nat.GCD.html#5894" class="Bound">n</a> <a id="5909" href="Data.Nat.GCD.html#5896" class="Bound">d</a> <a id="5911" class="Symbol">→</a> <a id="5913" href="Data.Nat.GCD.html#B%C3%A9zout.Identity.Identity" class="Datatype">Identity</a> <a id="5922" href="Data.Nat.GCD.html#5896" class="Bound">d</a> <a id="5924" href="Data.Nat.GCD.html#5892" class="Bound">m</a> <a id="5926" href="Data.Nat.GCD.html#5894" class="Bound">n</a>
  <a id="5930" href="Data.Nat.GCD.html#B%C3%A9zout.identity" class="Function">identity</a> <a id="5939" class="Symbol">{</a><a id="5940" href="Data.Nat.GCD.html#5940" class="Bound">m</a><a id="5941" class="Symbol">}</a> <a id="5943" class="Symbol">{</a><a id="5944" href="Data.Nat.GCD.html#5944" class="Bound">n</a><a id="5945" class="Symbol">}</a> <a id="5947" href="Data.Nat.GCD.html#5947" class="Bound">g</a> <a id="5949" class="Keyword">with</a> <a id="5954" href="Data.Nat.GCD.html#B%C3%A9zout.lemma" class="Function">lemma</a> <a id="5960" href="Data.Nat.GCD.html#5940" class="Bound">m</a> <a id="5962" href="Data.Nat.GCD.html#5944" class="Bound">n</a>
  <a id="5966" href="Data.Nat.GCD.html#B%C3%A9zout.identity" class="Function">identity</a> <a id="5975" href="Data.Nat.GCD.html#5975" class="Bound">g</a> <a id="5977" class="Symbol">|</a> <a id="5979" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma.result" class="InductiveConstructor">result</a> <a id="5986" href="Data.Nat.GCD.html#5986" class="Bound">d</a> <a id="5988" href="Data.Nat.GCD.html#5988" class="Bound">g′</a> <a id="5991" href="Data.Nat.GCD.html#5991" class="Bound">b</a> <a id="5993" class="Keyword">with</a> <a id="5998" href="Data.Nat.GCD.html#GCD.unique" class="Function">GCD.unique</a> <a id="6009" href="Data.Nat.GCD.html#5975" class="Bound">g</a> <a id="6011" href="Data.Nat.GCD.html#5988" class="Bound">g′</a>
  <a id="6016" href="Data.Nat.GCD.html#B%C3%A9zout.identity" class="Function">identity</a> <a id="6025" href="Data.Nat.GCD.html#6025" class="Bound">g</a> <a id="6027" class="Symbol">|</a> <a id="6029" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma.result" class="InductiveConstructor">result</a> <a id="6036" href="Data.Nat.GCD.html#6036" class="Bound">d</a> <a id="6038" href="Data.Nat.GCD.html#6038" class="Bound">g′</a> <a id="6041" href="Data.Nat.GCD.html#6041" class="Bound">b</a> <a id="6043" class="Symbol">|</a> <a id="6045" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">PropEq.refl</a> <a id="6057" class="Symbol">=</a> <a id="6059" href="Data.Nat.GCD.html#6041" class="Bound">b</a>

<a id="6062" class="Comment">-- Calculates the gcd of the arguments.</a>

<a id="gcd" href="Data.Nat.GCD.html#gcd" class="Function">gcd</a> <a id="6107" class="Symbol">:</a> <a id="6109" class="Symbol">(</a><a id="6110" href="Data.Nat.GCD.html#6110" class="Bound">m</a> <a id="6112" href="Data.Nat.GCD.html#6112" class="Bound">n</a> <a id="6114" class="Symbol">:</a> <a id="6116" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="6117" class="Symbol">)</a> <a id="6119" class="Symbol">→</a> <a id="6121" href="Data.Product.html#%E2%88%83" class="Function">∃</a> <a id="6123" class="Symbol">λ</a> <a id="6125" href="Data.Nat.GCD.html#6125" class="Bound">d</a> <a id="6127" class="Symbol">→</a> <a id="6129" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="6133" href="Data.Nat.GCD.html#6110" class="Bound">m</a> <a id="6135" href="Data.Nat.GCD.html#6112" class="Bound">n</a> <a id="6137" href="Data.Nat.GCD.html#6125" class="Bound">d</a>
<a id="6139" href="Data.Nat.GCD.html#gcd" class="Function">gcd</a> <a id="6143" href="Data.Nat.GCD.html#6143" class="Bound">m</a> <a id="6145" href="Data.Nat.GCD.html#6145" class="Bound">n</a> <a id="6147" class="Keyword">with</a> <a id="6152" href="Data.Nat.GCD.html#B%C3%A9zout.lemma" class="Function">Bézout.lemma</a> <a id="6165" href="Data.Nat.GCD.html#6143" class="Bound">m</a> <a id="6167" href="Data.Nat.GCD.html#6145" class="Bound">n</a>
<a id="6169" href="Data.Nat.GCD.html#gcd" class="Function">gcd</a> <a id="6173" href="Data.Nat.GCD.html#6173" class="Bound">m</a> <a id="6175" href="Data.Nat.GCD.html#6175" class="Bound">n</a> <a id="6177" class="Symbol">|</a> <a id="6179" href="Data.Nat.GCD.html#B%C3%A9zout.Lemma.Lemma.result" class="InductiveConstructor">Bézout.result</a> <a id="6193" href="Data.Nat.GCD.html#6193" class="Bound">d</a> <a id="6195" href="Data.Nat.GCD.html#6195" class="Bound">g</a> <a id="6197" class="Symbol">_</a> <a id="6199" class="Symbol">=</a> <a id="6201" class="Symbol">(</a><a id="6202" href="Data.Nat.GCD.html#6193" class="Bound">d</a> <a id="6204" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6206" href="Data.Nat.GCD.html#6195" class="Bound">g</a><a id="6207" class="Symbol">)</a>

<a id="6210" class="Comment">-- gcd as a proposition is decidable</a>

<a id="gcd?" href="Data.Nat.GCD.html#gcd%3F" class="Function">gcd?</a> <a id="6253" class="Symbol">:</a> <a id="6255" class="Symbol">(</a><a id="6256" href="Data.Nat.GCD.html#6256" class="Bound">m</a> <a id="6258" href="Data.Nat.GCD.html#6258" class="Bound">n</a> <a id="6260" href="Data.Nat.GCD.html#6260" class="Bound">d</a> <a id="6262" class="Symbol">:</a> <a id="6264" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="6265" class="Symbol">)</a> <a id="6267" class="Symbol">→</a> <a id="6269" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="6273" class="Symbol">(</a><a id="6274" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="6278" href="Data.Nat.GCD.html#6256" class="Bound">m</a> <a id="6280" href="Data.Nat.GCD.html#6258" class="Bound">n</a> <a id="6282" href="Data.Nat.GCD.html#6260" class="Bound">d</a><a id="6283" class="Symbol">)</a>
<a id="6285" href="Data.Nat.GCD.html#gcd%3F" class="Function">gcd?</a> <a id="6290" href="Data.Nat.GCD.html#6290" class="Bound">m</a> <a id="6292" href="Data.Nat.GCD.html#6292" class="Bound">n</a> <a id="6294" href="Data.Nat.GCD.html#6294" class="Bound">d</a> <a id="6296" class="Keyword">with</a> <a id="6301" href="Data.Nat.GCD.html#gcd" class="Function">gcd</a> <a id="6305" href="Data.Nat.GCD.html#6290" class="Bound">m</a> <a id="6307" href="Data.Nat.GCD.html#6292" class="Bound">n</a>
<a id="6309" class="Symbol">...</a> <a id="6313" class="Symbol">|</a> <a id="6315" href="Data.Nat.GCD.html#6315" class="Bound">d′</a> <a id="6318" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6320" href="Data.Nat.GCD.html#6320" class="Bound">p</a> <a id="6322" class="Keyword">with</a> <a id="6327" href="Data.Nat.GCD.html#6315" class="Bound">d′</a> <a id="6330" href="Data.Nat.Base.html#_%E2%89%9F_" class="Function Operator">≟</a> <a id="6332" class="Bound">d</a>
<a id="6334" class="Symbol">...</a> <a id="6338" class="Symbol">|</a> <a id="6340" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="6343" href="Data.Nat.GCD.html#6343" class="Bound">¬g</a> <a id="6346" class="Symbol">=</a> <a id="6348" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="6351" class="Symbol">(λ</a> <a id="6354" href="Data.Nat.GCD.html#6354" class="Bound">p′</a> <a id="6357" class="Symbol">→</a> <a id="6359" href="Data.Nat.GCD.html#6343" class="Bound">¬g</a> <a id="6362" class="Symbol">(</a><a id="6363" href="Data.Nat.GCD.html#GCD.unique" class="Function">GCD.unique</a> <a id="6374" class="Bound">p</a> <a id="6376" href="Data.Nat.GCD.html#6354" class="Bound">p′</a><a id="6378" class="Symbol">))</a>
<a id="6381" class="Symbol">...</a> <a id="6385" class="Symbol">|</a> <a id="6387" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="6391" href="Data.Nat.GCD.html#6391" class="Bound">g</a> <a id="6393" class="Symbol">=</a> <a id="6395" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="6399" class="Symbol">(</a><a id="6400" href="Relation.Binary.PropositionalEquality.Core.html#subst" class="Function">subst</a> <a id="6406" class="Symbol">(</a><a id="6407" href="Data.Nat.GCD.html#GCD.GCD" class="Record">GCD</a> <a id="6411" class="Bound">m</a> <a id="6413" class="Bound">n</a><a id="6414" class="Symbol">)</a> <a id="6416" href="Data.Nat.GCD.html#6391" class="Bound">g</a> <a id="6418" class="Bound">p</a><a id="6419" class="Symbol">)</a>
</pre></body></html>

APT Browse - Built by Thomas Orozco.