我正在学习精益教程的第 4 章。
我希望能够证明简单的等式，例如a = b ? a + 1 = b + 1 无需使用 calc 环境。换句话说，我想明确构建以下证明项：
example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := sorry
我最好的猜测是我需要使用eq.subst标准库中关于自然数相等的一些相关引理，但我不知所措。我能找到的最接近的精益例子是这样的：
example (A : Type) (a b : A) (P : A ? Prop) (H1 : a = b) (H2 : P a) : P b :=
eq.subst H1 H2