This lemma is false. If you try with n = nx = 0 (e.g. using destruct n and destruct nx) and simplify, you get 0 <= 0 -> 1 = 0.
n = nx = 0
destruct n
destruct nx
0 <= 0 -> 1 = 0