## Stream: new members

### Topic: naturals nonnegative

#### Alex Kontorovich (Mar 11 2020 at 15:38):

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


#### Reid Barton (Mar 11 2020 at 15:42):

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

#### Reid Barton (Mar 11 2020 at 15:42):

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

#### Alex Kontorovich (Mar 11 2020 at 16:02):

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 (Mar 11 2020 at 16:02):

exfalso

#### Kevin Buzzard (Mar 11 2020 at 16:18):

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


There are no cases to consider :-)

Last updated: May 14 2021 at 13:24 UTC