Coq proving addition inequality

Question

I am a beginner and trying to prove this lemma:

Lemma test:  forall n m p q : nat,
    n <= p \/ m <= q -> n + m <= p + q.

I tried

From Coq Require Export Lia.

Lemma test:  forall n m p q : nat,
        n <= p \/ m <= q -> n + m <= p + q
Proof.
    intros; omega.

and Lia, but it is not working. How could I proceed?

Answer 1

You probably meant

Lemma test:  forall n m p q : nat,
    n <= p /\ m <= q -> n + m <= p + q.

with /\ (logical and) rather than \/ (logical or) because your theorem does not hold otherwise. As a counterexample, pick n = p = q = 0 and m = 1.

When fixed that way, lia finds the proof automatically.

Also, note it is more idiomatic in Coq to currify types, that is replacing conjunction on the left of an arrow with an arrow. This would read

Lemma test:  forall n m p q : nat,
    n <= p -> m <= q -> n + m <= p + q.

which is equivalent.

Answer 2

Thank you for the answer. However,

Proof.
  intros. lia.

gives:

Error: Tactic failure:  Cannot find witness.

Is there a way to proceed?