我正在尝试完成逻辑基础关于归纳命题一章的系列练习le_exercises。
这个系列主要基于归纳关系le，定义如下：
Inductive le : nat -> nat -> Prop :=
| le_n (n : nat) : le n n
| le_S (n m : nat) (H : le n m) : le n (S m).
Notation "n <= m" := (le n m).
我坚持的特定定理如下：
Theorem add_le_cases : forall n m p q,
n + m <= p + q -> n <= p \/ m <= q.
到目前为止，我设法证明的这些系列中的先前定理是：
Lemma le_trans : ∀ m n o, m ≤ n → n ≤ o → m ≤ o.
Theorem O_le_n : ∀ n, 0 ≤ n.
Theorem n_le_m__Sn_le_Sm : ∀ n m, n ≤ m → S n ≤ S m.
Theorem Sn_le_Sm__n_le_m : ∀ n m, S n ≤ S m → n ≤ m.
Theorem lt_ge_cases : ∀ n m, n < m ∨ n ≥ m.
Theorem le_plus_l : ∀ a b, a ≤ a + b.
Theorem plus_le : ∀ n1 n2 m, n1 + n2 ≤ m → n1 ≤ m ∧ n2 ≤ m.
这本书给出了一个提示，指出该定理add_le_cases可能“更容易通过归纳证明n”，我以各种方式尝试过，但似乎无处可去。
Theorem add_le_cases : forall n m p q,
n + m <= p + q -> n <= p \/ m <= q.
Proof.
intros n. induction n.
- intros. left. apply O_le_n.
- intros. inversion H.
+ destruct m.
* right. apply O_le_n.
* (* stuck *)
我考虑过使用该plus_le定理，但似乎无法从中获得任何有用的信息。我觉得我的理解中肯定缺少一些重要的东西，但你不知道你不知道什么。