ForMatUS: El máximo común divisor de m y n es igual a m si, y sólo si, m divide a n (en Lean)

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo El máximo común divisor de m y n es igual a m si, y sólo si, m divide a n (en Lean) en el que se comenta la prueba en Lean de la siguiente propiedad de los números naturales: el máximo común divisor de a y b es igual a a si, y sólo si, a divide a b. Más concretamente,

Sean m y n son números naturales. Entonces, son equivalentes

mcd(m,n) = n

m divide a n

Su enunciado en Lean es

import data.nat.gcd

open nat

variables (a b : ℕ)

example : a ∣ b ↔ gcd a b = a :=
sorry

import data.nat.gcd

open nat

variables (a b : ℕ)

example : a ∣ b ↔ gcd a b = a :=

sorry

En la demostración se utilizan los siguientes propiedades de los números naturales:

dvd_refl:      a ∣ a
dvd_antisymm : a ∣ b → b ∣ a → a = b 
dvd_gcd_iff :  c ∣ gcd a b ↔ c ∣ a ∧ c ∣ b
gcd_dvd :      gcd a b ∣ a ∧ gcd a b ∣ b

dvd_refl: a ∣ a

dvd_antisymm : a ∣ b → b ∣ a → a = b

dvd_gcd_iff : c ∣ gcd a b ↔ c ∣ a ∧ c ∣ b

gcd_dvd : gcd a b ∣ a ∧ gcd a b ∣ b

Los enlaces correspondientes son:

A continuación, se muestra el vídeo