/-- Addition cancellation should use the hypothesis and library cancellation theorem. -/
theorem addLeftCancelBuiltin (a b c : Nat) (h : a + b = a + c) : b = c := by
{{PROOF}}