a b : Int
h : 0 ≤ b
this : 0 + a ≤ b + a
⊢ a ≤ b + a
a b : Int
h : 0 ≤ b
⊢ a ≤ b + a
have : 0 + a ≤ b + a := Int.add_le_add_right h a
no goals
a b : Int
h : 0 ≤ b
this : 0 + a ≤ b + a
⊢ a ≤ b + a
rwa [Int.zero_add] at this