软件基础（lf）：证明leb_plus_exists和plus_leb_exists

Question

我一直在学习《软件基础》第一卷，但我无法通过 Logic.v 中的一对可选问题。有人知道该怎么做吗？

定理 leb_plus_exists ：对于所有 n m，n <=? m = true -> 存在 x，m = n+x。 证明。 承认了。

定理 plus_exists_leb : forall n m, (存在 x, m = n+x) -> n <=? m = true. Proof. (* FILL IN HERE *) Admitted.

我无法理解第一个问题中的介绍。我完全不知道该怎么办。

Answer 1

请注意，软件基础练习的解决方案，尤其是第 1 卷：逻辑基础，不会发布。

因此，这里有一个提示：在执行

induction n

之前执行 intros m

，这会将所有声明 

general 保留在 m

 中。

或者，这里没有必要，但如果您首先完成所有

intros

，那么您需要

generalize dependent m

：请参阅

概括依赖。