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: Open

Submit Your Proof

Back to Bounties