Conmutatividad del máximo común divisor
Demostrar con Lean4 que si \(m, n \in \mathbb{N}\) son números naturales, entonces
\[\gcd(m, n) = \gcd(n, m)\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable (k m n : ℕ) open Nat example : gcd m n = gcd n m := by sorry |