rw [Int.neg_negSucc, Int.neg_negSucc, Int.ofNat_lt] at this
x x' : ℕ
h : Int.negSucc x < Int.negSucc x'
this : -Int.negSucc x' < -Int.negSucc x
⊢ x' < x
x x' : ℕ
h : Int.negSucc x < Int.negSucc x'
this : x'.succ < x.succ
⊢ x' < x