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

State before:
i : Int
k : Nat
⊢ (i + ↑k - i).NonNeg
Tactic:
rw [Int.sub_eq, Int.add_right_comm, Int.add_neg_self_right, Int.zero_add]
State after:
i : Int
k : Nat
⊢ (↑k).NonNeg

State before:
i : Int
k : Nat
⊢ (↑k).NonNeg
Tactic:
apply NonNeg.mk
State after:
no goals