Zulip Chat Archive

Stream: new members

Topic: n % 2 = 1


view this post on Zulip Huỳnh Trần Khanh (Feb 09 2021 at 02:29):

How do I prove this?

example { n :  } (h : ¬(n % 2 = 0)) : n % 2 = 1 := begin
  sorry,
end

view this post on Zulip Bryan Gin-ge Chen (Feb 09 2021 at 02:35):

import data.nat.parity

example { n :  } (h : ¬(n % 2 = 0)) : n % 2 = 1 := begin
  rwa [ nat.odd_iff, nat.odd_iff_not_even, nat.even_iff],
end

view this post on Zulip Mario Carneiro (Feb 09 2021 at 02:46):

example {n : } (h : ¬(n % 2 = 0)) : n % 2 = 1 :=
(nat.mod_two_eq_zero_or_one _).resolve_left h

view this post on Zulip Mario Carneiro (Feb 09 2021 at 02:46):

that doesn't even need imports, the lemma is in core

view this post on Zulip Mario Carneiro (Feb 09 2021 at 02:47):

(although I highly doubt it needs to be)

view this post on Zulip Huỳnh Trần Khanh (Feb 09 2021 at 03:44):

Thanks! I just completed the CSES Counting Bits proof thanks to your help. In a minute or two I'll post a proof review request!


Last updated: May 14 2021 at 00:42 UTC