Zulip Chat Archive

Stream: new members

Topic: naturals nonnegative


view this post on Zulip Alex Kontorovich (Mar 11 2020 at 15:38):

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

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Mar 11 2020 at 15:42):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 11 2020 at 16:02):

exfalso

view this post on Zulip 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