IndProp.v

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.