小编use*_*206的帖子

我正在努力完成逻辑基础归纳命题章节中le_exercises的一系列练习。

该系列主要基于归纳关系le，定义如下：

Inductive le : nat -> nat -> Prop :=\n  | le_n (n : nat)                : le n n\n  | le_S (n m : nat) (H : le n m) : le n (S m).\n\nNotation "n <= m" := (le n m).\n

我所坚持的特定定理如下：

Theorem add_le_cases : forall n m p q,\n  n + m <= p + q -> n <= p \\/ m <= q.\n

到目前为止我成功证明的本系列中的先前定理是：

Lemma le_trans …