theorem-proving - 定数が関係している場合、リーン定理証明器で型を切り替える方法は?

Question

LEAN ドキュメンテーションに取り組んでいる新参者にとって、より困難な問題が解決されたように見えるときに、いくつかの単純な問題が実際のボトルネックに変わるのを見ると、非常にイライラすることがあります。これは、数時間の欲求不満に変わった単純な自作の演習であると思われていたものです（もちろん、学ぶには他に方法はありません）：

theorem prByCont : ∀ P : Prop, ( P → false ) → ¬ P :=
    λ (P : Prop) (prf : P → false), prf
#check prByCont

example ( a b : ℕ ) (p: a = 2) (q: b=3) : ¬ (a ≥ b) :=
begin
    apply prByCont,
    assume h : a ≥ b,
    have order : 2 < 3 := dec_trivial,
    contradiction
end

問題は that orderhas typeの2<3ようですが、必要なのは であり、とa<bが明確であるように私には見えますが、LEAN はそうは考えていません。ここで何が欠けているかを教えてください！a=2b=3