GCDs and Bezout's theorem

[siddhartha-gadgil]

Euclid's algorithm extending to Bezout's lemma gives for natural numbers a and b

• a natural number d
• proofs that d divides a and d divides b
• integers k and l with d = a k + b l
  As a consequence, we also have that if c divides both a and b, then it divides d

[NabarunDeka]

I created a file called gcd.idr, where i put a proof of divisibility. Can someone please check it once. Thank You.

[siddhartha-gadgil]

It is better to just use a dependent pair like the one in lectures/homework for being even, so one gets the factor directly.

…

On Thu, Jan 24, 2019 at 11:55 AM NabarunDeka ***@***.***> wrote: I created a file called gcd.idr, where i put a proof of divisibility. Can someone please check it once. Thank You. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#3 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ADatpBBOxpM9BrtFLmRirtpSvcxqZi4yks5vGVHKgaJpZM4aOC8q> .

[siddhartha-gadgil]

I have added a Sigma-type for defining divisibility in Intro.idr in commit ba62878 - works need to be done working inductively for sums and products