gcd 関数の停止証明

[Seasawher]

gcd 関数が停止することの証明がわからないのですが，以下の sorry を埋めるにはどうしたらいいでしょうか？

(lean4 web で再現してください)

import Mathlib

def gcd : (a : Nat) → (b : Nat) → Nat
  | a, 0 => a
  | a, b =>
    have : a % b < b := by
      sorry
    gcd b (a % b)
termination_by _ a b => b

調べると，Mechanics of Proof では gcd 関数が停止することの証明にいくつか補題を用意していますが，そこまで準備しなくても示せるはずでは？と思っています

https://hrmacbeth.github.io/math2001/06_Induction.html?highlight=gcd#the-euclidean-algorithm

[Seasawher]

これで通るようです．Leanは，パターンマッチでそれまでのケースに当てはまらないという仮定を追加してくれないのでしょうか…？

import Mathlib.Tactic

def gcd : (a : Nat) → (b : Nat) → Nat
  | a, 0 => a
  | a, k + 1 =>
    let b := k + 1
    have : a % b < b := by
      refine Nat.mod_lt a ?_
      linarith
    gcd b (a % b)
termination_by _ a b => b