n % 2 = 1

Stream: new members

[Huỳnh Trần Khanh]

How do I prove this?

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

[Bryan Gin-ge Chen]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

(although I highly doubt it needs to be)

[Huỳnh Trần Khanh]

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!