## Stream: new members

### Topic: n % 2 = 1

#### 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


#### 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


#### 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


#### Mario Carneiro (Feb 09 2021 at 02:46):

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

#### Mario Carneiro (Feb 09 2021 at 02:47):

(although I highly doubt it needs to be)

#### 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