naturals nonnegative

Stream: new members

[Alex Kontorovich]

Can someone please help me turn this into "false"?

n : ℕ,
p : 0 > n
⊢ Σ' (k : ℕ), k + n = 0

[Reid Barton]

I would try have : not (0 > n), by library_search, and see what it prints, probably something like not_lt_zero.

[Reid Barton]

linarith should be able to do it too, but that's overkill

[Alex Kontorovich]

Thanks! But now I can't seem to finish it from "false" ... Help please?

lemma subtraction (m n : ℕ) (p : m > n) : Σ' k, k + n = m
:=
begin
induction m,
let contr:= nat.not_lt_zero n p,
sorry,
end

[Kenny Lau]

exfalso

[Kevin Buzzard]

example (n : ℕ) (p : 0 > n) : 2 + 2 = 5 :=
begin
  cases p,
end

There are no cases to consider :-)