a : Int
h : 0 ≤ a
t : ∃ n, a - 0 = ↑n
⊢ ∃ n, a = ↑n
a : Int
h : 0 ≤ a
⊢ ∃ n, a = ↑n
have t := le.dest_sub h
a : Int
h : 0 ≤ a
t : ∃ n, a = ↑n
⊢ ∃ n, a = ↑n
a : Int
h : 0 ≤ a
t : ∃ n, a - 0 = ↑n
⊢ ∃ n, a = ↑n
simp [Int.sub_eq_add_neg] at t
no goals
a : Int
h : 0 ≤ a
t : ∃ n, a = ↑n
⊢ ∃ n, a = ↑n
exact t