Skip to content

Instantly share code, notes, and snippets.

@ysangkok
Created December 16, 2020 19:50
Show Gist options
  • Save ysangkok/aeead93cc53431f376b54671e0d7c2f4 to your computer and use it in GitHub Desktop.
Save ysangkok/aeead93cc53431f376b54671e0d7c2f4 to your computer and use it in GitHub Desktop.
Theorem add_le_cases : forall (n: nat) (m: nat) (p: nat) (q: nat),
n + m <= p + q -> n <= p \/ m <= q.
Proof.
intros.
generalize dependent p.
induction n.
- simpl.
intros.
apply or_introl.
apply le_0_n.
- intros.
destruct p.
* apply or_intror.
rewrite plus_O_n in H.
simpl in H.
assert (canremoveS: S (n + m) <= q -> n + m <= q) by admit.
apply canremoveS in H.
apply plus_le in H.
apply proj2 in H.
apply H.
* assert (canaddSTwice: n <= p \/ m <= q -> S n <= S p \/ m <= q) by admit.
apply canaddSTwice.
apply IHn.
simpl in H.
apply le_S_n in H.
apply H.
ed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment