no goals
a b c : Nat
h : a + b ≤ a + c
⊢ b ≤ c
match le.dest h with
| ⟨d, hd⟩ =>
  apply @le.intro _ _ d
  rw [Nat.add_assoc] at hd
  apply Nat.add_left_cancel hd
a b c : Nat
h : a + b ≤ a + c
d : Nat
hd : a + b + d = a + c
⊢ b + d = c
a b c : Nat
h : a + b ≤ a + c
d : Nat
hd : a + b + d = a + c
⊢ b ≤ c
apply @le.intro _ _ d
a b c : Nat
h : a + b ≤ a + c
d : Nat
hd : a + (b + d) = a + c
⊢ b + d = c
a b c : Nat
h : a + b ≤ a + c
d : Nat
hd : a + b + d = a + c
⊢ b + d = c
rw [Nat.add_assoc] at hd
no goals
a b c : Nat
h : a + b ≤ a + c
d : Nat
hd : a + (b + d) = a + c
⊢ b + d = c
apply Nat.add_left_cancel hd