no goals
a b : Nat
⊢ a - b + b = max a b
match a.le_total b with
| .inl hl => rw [Nat.max_eq_right hl, Nat.sub_eq_zero_iff_le.mpr hl, Nat.zero_add]
| .inr hr => rw [Nat.max_eq_left hr, Nat.sub_add_cancel hr]
no goals
a b : Nat
hl : a ≤ b
⊢ a - b + b = max a b
rw [Nat.max_eq_right hl, Nat.sub_eq_zero_iff_le.mpr hl, Nat.zero_add]
no goals
a b : Nat
hr : b ≤ a
⊢ a - b + b = max a b
rw [Nat.max_eq_left hr, Nat.sub_add_cancel hr]