a b : Int
h✝ : 0 < a - b
h : 0 + b < a - b + b
⊢ b < a
a b : Int
h : 0 < a - b
⊢ b < a
have h := Int.add_lt_add_right h b
no goals
a b : Int
h✝ : 0 < a - b
h : 0 + b < a - b + b
⊢ b < a
rwa [Int.sub_add_cancel, Int.zero_add] at h