English
For Nat a,b with a ≤ b and a bound on natSize, gcdAux n a b equals Nat.gcd a b when cast to ℕ.
Русский
Для чисел Nat a,b соотношения a ≤ b и ограничение natSize приводят к тому, что gcdAux n a b, приведённый к ℕ, равен Nat.gcd a b.
LaTeX
$$$\forall n: Nat,\; \forall a,b: Num,\; Num.instLE.le\ a\ b \land (a*b).natSize \le n \Rightarrow (gcdAux n a b : \mathbb{N}) = Nat.gcd a b$$$
Lean4
theorem gcd_to_nat_aux : ∀ {n} {a b : Num}, a ≤ b → (a * b).natSize ≤ n → (gcdAux n a b : ℕ) = Nat.gcd a b
| 0, 0, _, _ab, _h => (Nat.gcd_zero_left _).symm
| 0, pos _, 0, ab, _h => (not_lt_of_ge ab).elim rfl
| 0, pos _, pos _, _ab, h => (not_lt_of_ge h).elim <| PosNum.natSize_pos _
| Nat.succ _, 0, _, _ab, _h => (Nat.gcd_zero_left _).symm
| Nat.succ n, pos a, b, ab, h => by
simp only [gcdAux, cast_pos]
rw [Nat.gcd_rec, gcd_to_nat_aux, mod_to_nat]
· rfl
· rw [← le_to_nat, mod_to_nat]
exact le_of_lt (Nat.mod_lt _ (PosNum.cast_pos _))
rw [natSize_to_nat, mul_to_nat, Nat.size_le] at h ⊢
rw [mod_to_nat, mul_comm]
rw [pow_succ, ← Nat.mod_add_div b (pos a)] at h
refine lt_of_mul_lt_mul_right (lt_of_le_of_lt ?_ h) (Nat.zero_le 2)
rw [mul_two, mul_add]
refine add_le_add_left (Nat.mul_le_mul_left _ (le_trans (le_of_lt (Nat.mod_lt _ (PosNum.cast_pos _))) ?_)) _
suffices 1 ≤ _ by simpa using Nat.mul_le_mul_left (pos a) this
rw [Nat.le_div_iff_mul_le a.cast_pos, one_mul]
exact le_to_nat.2 ab
