Seeming contradiction

Stream: new members

[Maris Ozols]

I am trying to prove something very simple and I stumbled upon the following "result":

theorem what
  (a b N : Nat)
  : a - N * ((a + b) / N) ≥ 0 := by linarith

This seems like a contradiction to me because if N = 1 and b = 1 this would imply -1 ≥ 0. Am I misunderstanding something?

[Ilmārs Cīrulis]

It's because Nat subtraction stops at 0.

[Maris Ozols]

OK, thanks.

[Kevin Buzzard]

If you use naturals you'll get results in naturals, whether you like it or not. If you want negative numbers as outputs, you can use integers, and if you want some of them to be non-negative you can just put a >= 0 as a hypothesis. This is a common beginner "gotcha", that 0 - 1 =0 for naturals. It's because the type of subtraction is A -> A -> A, i.e. if you give it two naturals it must return a natural. Note that division is equally weird -- 5 / 2 = 2 for example, for the same reason. If you want a working division as well then use rationals.

[Ben Eltschig]

Also note that if you have natural numbers a,b, you can still subtract them and get an integer by explicity annotating the type as (a - b : ℤ), (a : ℤ) - b or a - (b : ℤ) - in all three cases, a and b will both get converted to integers before the subtraction happens. So you don't need to already have integers if you want integer subtraction, you just need to tell lean at some point that you don't want to stay in $\mathbb N$.