n m : Nat
h : n ≤ m
k : Nat
⊢ k + n ≤ k + m
n m : Nat
h : n ≤ m
k : Nat
⊢ n + k ≤ m + k
rw [Nat.add_comm n k, Nat.add_comm m k]
case h
n m : Nat
h : n ≤ m
k : Nat
⊢ n ≤ m
n m : Nat
h : n ≤ m
k : Nat
⊢ k + n ≤ k + m
apply Nat.add_le_add_left
no goals
case h
n m : Nat
h : n ≤ m
k : Nat
⊢ n ≤ m
assumption