a b : Int
h : 0 ≤ b
this : a + b ≥ a + 0
⊢ a ≤ a + b
a b : Int
h : 0 ≤ b
⊢ a ≤ a + b
have : a + b ≥ a + 0 := Int.add_le_add_left h a
no goals
a b : Int
h : 0 ≤ b
this : a + b ≥ a + 0
⊢ a ≤ a + b
rwa [Int.add_zero] at this