涉及常数时如何在Lean定理证明者中切换类型？

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

问题似乎是order的类型为2<3，但需要的是a<b，尽管在我看来a=2和b=3应该很清楚，但LEAN并不认为所以。请帮助我看看我在这里缺少什么！

Answer 1

dec_trivial仅在语句中没有可用变量时起作用。因此，如果语句中存在变量a，则dec_trivial将不起作用。我认为证明rw [q, p], exact dec_trivial将起作用，因为在重写之后，目标中没有变量。