English
The gcd of two Num numbers, when viewed as a Nat, equals the Nat gcd of the extracted integers, i.e., gcd(a,b) corresponds to Nat.gcd after casting.
Русский
Наибольший общий делитель двух чисел Num при приведении к Nat равен обычному gcd в Nat: gcd(a,b) = Nat.gcd(a,b).
LaTeX
$$$\forall a,b: Num, (gcd\ a\ b : \mathbb{N}) = Nat.gcd\ a\ b$$$
Lean4
@[simp]
theorem gcd_to_nat : ∀ a b, (gcd a b : ℕ) = Nat.gcd a b :=
by
have : ∀ a b : Num, (a * b).natSize ≤ a.natSize + b.natSize :=
by
intros
simp only [natSize_to_nat, cast_mul]
rw [Nat.size_le, pow_add]
exact mul_lt_mul'' (Nat.lt_size_self _) (Nat.lt_size_self _) (Nat.zero_le _) (Nat.zero_le _)
intros
unfold gcd
split_ifs with h
· exact gcd_to_nat_aux h (this _ _)
· rw [Nat.gcd_comm]
exact gcd_to_nat_aux (le_of_not_ge h) (this _ _)
