exact Nat.add_left_cancel h