I am trying to complete the series of exercises le_exercises from Logical Foundations' chapter on inductive propositions.
This series is mostly based on the inductive relation le, defined thusly:
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).
The particular theorem I am stuck at is the following:
Theorem add_le_cases : forall n m p q,
n + m <= p + q -> n <= p \/ m <= q.
The previous theorems in these series that I managed to prove so far are:
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.
The book gives a hint stating that the theorem add_le_cases may be "easier to prove by induction on n" which I tried in various ways, but can't seem to go anywhere.
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 *)
I have considered using the plus_le theorem but can't seem to get anything useful from it. I feel there must be something crucial missing from my understanding but you can't know what you don't know.
Well, I would not do inversion H and destruct m. I would just destruct p and after solving the O case, then massage H a bit to be able to apply the induction hypothesis.