Theorem Marketplace

Theorem Details

import Mathlib.Data.Nat.GCD.Basic

-- Prove that gcd(a, b) = gcd(b, a % b)

theorem gcd_eq_gcd_mod (a b : ℕ) (h : b ≠ 0) : Nat.gcd a b = Nat.gcd b (a % b) := by sorry

Bounty: 0.02 ETH

Status: Closed

Proof

import Mathlib.Data.Nat.GCD.Basic

-- Prove that gcd(a, b) = gcd(b, a % b)

theorem gcd_eq_gcd_mod (a b : ℕ) (h : b ≠ 0) : Nat.gcd a b = Nat.gcd b (a % b) := by {
  symm
  rw [Nat.gcd_eq_iff]
  split_ands
  exact Nat.gcd_dvd_right a b
  {
    rw [Nat.dvd_mod_iff]
    exact Nat.gcd_dvd_left a b
    exact Nat.gcd_dvd_right a b
  }
  intro c h1 h2
  rw [Nat.dvd_mod_iff h1] at h2
  exact Nat.dvd_gcd h2 h1
}

Back to Bounties