Greatest_Common_Divisor_is_at_least_1
Disprovedgreatest-common-divisorproofwiki
The greatest common divisor of any two integers is at least 1.
Preamble
import Mathlib.Data.Int.GCD
Formal statement
theorem Greatest_Common_Divisor_is_at_least_1 (a b : ℤ) : 1 ≤ Int.gcd a b := by sorry
Source