Theorem: Imo2012P4.Int.lt_of_ns_lt_ns (Compfiles/Imo2012P4.lean)

State before:
x x' : ℕ
h : Int.negSucc x < Int.negSucc x'
⊢ x' < x
Tactic:
have := Int.neg_lt_neg h
State after:
x x' : ℕ
h : Int.negSucc x < Int.negSucc x'
this : -Int.negSucc x' < -Int.negSucc x
⊢ x' < x

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

State before:
x x' : ℕ
h : Int.negSucc x < Int.negSucc x'
this : x'.succ < x.succ
⊢ x' < x
Tactic:
apply Nat.lt_of_succ_lt_succ this
State after:
no goals