Reduce unable to solve simple inequalities with quantifiers

Question

I have try to solve following inequalities using Mamthematica. But it unable to solve that.

Reduce[ForAll[{n}, Implies[{n, N1} >= 0 && n < N1, n < A]] && 
  N1 >= A, {N1,A}, Integers]

Expected Result

N1=A

If we solve that manually,it is very simple.Please Suggest . am I making any mistake or other way to handle this type of problem?

Answer 1

The way you defined the conditions is a little bit hazy to me. For example consider {n, N1} >= 0 && n < N1. The first condition does not do anything to N1. In fact,

Reduce[{n, N1} >= 0 && n < N1, {n, N1}]

n >= 0 && N1 > n

So you can simply combine them to N1>0. Make this modification in your first condition, and you will get

Reduce[0 < N1 && 0 < A && N1 >= A, {N1, A}, Integers]

(C[1] | C[2]) [Element] Integers && C[1] >= 0 && C[2] >= 0 && N1 == 1 + C[1] + C[2] && A == 1 + C[2]

and for C[1]=0 you get your desired answer.