GCD_with_Remainder
Provedgreatest-common-divisorproofwiki
Let a, b, q, r be integers such that a = qb + r. Then gcd(a, b) = gcd(b, r).
Preamble
import Mathlib.Data.Int.GCD
Formal statement
theorem GCD_with_Remainder (a b q r : ℤ) (h : a = q * b + r) : Int.gcd a b = Int.gcd b r := by sorry
Source