How to prove Theorem plus_lt : forall n1 n2 m, n1 + n2 < m -> n1 < m /\ n2 < m

Question

Here I am with another doubt on how to prove theorems in coq. This is as far as I got:

Theorem plus_lt : forall n1 n2 m,
  n1 + n2 < m ->
  n1 < m /\ n2 < m.
Proof.
  intros n1.
  induction n2 as [| n2' IHn2'].
  - intros m H. inversion H.
    + split.
      * unfold lt. rewrite add_0_r. 
        apply n_le_m__Sn_le_Sm. apply le_n.
      * unfold lt. rewrite add_0_r.
        apply n_le_m__Sn_le_Sm. apply O_le_n.
    + split.
      * rewrite add_0_r in H. rewrite H1. apply H.
      * unfold lt. apply n_le_m__Sn_le_Sm. apply O_le_n.
  - intros m H. 
    + induction m as [| m' IHm'].
      * unfold lt. apply n_le_m__Sn_le_Sm in H. apply Sn_le_Sm__n_le_m in H.
        rewrite add_comm in H. rewrite plus_n_Sm in H.
        inversion H.
      * inversion H.
        ++ rewrite H1. unfold lt in H. apply Sn_le_Sm__n_le_m in H.
           apply plus_le in H. unfold lt. destruct H. split.
           ** apply n_le_m__Sn_le_Sm. apply H.
           ** apply n_le_m__Sn_le_Sm. apply H0.
        ++ unfold lt in H. rewrite add_comm in H. rewrite plus_n_Sm in H.
           apply plus_le in H. destruct H. split.
           ** unfold lt. apply H2.
           ** unfold lt. 

But the longer I stare at it, the more I realize that there has to be a much simpler way to prove this. Every avenue I tried end up with in a road block, something I can't prove. Here are my current goals:

  n1, n2' : nat
  IHn2' : forall m : nat, n1 + n2' < m -> n1 < m /\ n2' < m
  m' : nat
  H : S n2' <= S m'
  H2 : S n1 <= S m'
  IHm' : n1 + S n2' < m' -> n1 < m' /\ S n2' < m'
  m : nat
  H1 : S (n1 + S n2') <= m'
  H0 : m = m'
  ============================
  S (S n2') <= S m'

I mean, the size of this proof already tells me that I must have gone super wrong somewhere. The fact is far too clear to take these many steps. I have been at this little thing for over 8 hours already :-p

Hopefully one day I'll get the hang of it :-)

Thanks

Answer 1

You may also want to split the goal and then use transitivity of inequality with n_1 and n_1 + n_2. Idem for n_2.