Theorem: Int.le.dest' (GMLInit/Data/Int.lean)

State before:
i j : Int
⊢ i ≤ j → ∃ k, j = i + ofNat k
Tactic:
intro (h : NonNeg (j - i))
State after:
i j : Int
h : (j - i).NonNeg
⊢ ∃ k, j = i + ofNat k

State before:
i j : Int
h : (j - i).NonNeg
⊢ ∃ k, j = i + ofNat k
Tactic:
match hk : j - i with
| ofNat k => exists k; rw [←hk, Int.sub_eq, Int.add_left_comm, Int.add_neg_self_right, Int.add_zero]
| negSucc _ => rw [hk] at h; contradiction
State after:
no goals

State before:
i j : Int
h : (j - i).NonNeg
k : Nat
hk : j - i = ofNat k
⊢ ∃ k, j = i + ofNat k
Tactic:
exists k
State after:
i j : Int
h : (j - i).NonNeg
k : Nat
hk : j - i = ofNat k
⊢ j = i + ofNat k

State before:
i j : Int
h : (j - i).NonNeg
k : Nat
hk : j - i = ofNat k
⊢ j = i + ofNat k
Tactic:
rw [←hk, Int.sub_eq, Int.add_left_comm, Int.add_neg_self_right, Int.add_zero]
State after:
no goals

State before:
i j : Int
h : (j - i).NonNeg
a✝ : Nat
hk : j - i = -[a✝+1]
⊢ ∃ k, j = i + ofNat k
Tactic:
rw [hk] at h
State after:
i j : Int
a✝ : Nat
h : -[a✝+1].NonNeg
hk : j - i = -[a✝+1]
⊢ ∃ k, j = i + ofNat k

State before:
i j : Int
a✝ : Nat
h : -[a✝+1].NonNeg
hk : j - i = -[a✝+1]
⊢ ∃ k, j = i + ofNat k
Tactic:
contradiction
State after:
no goals