example (x : Int) : x % 2 = 0 ∨ x % 2 = 1 := by sorry

Stream: Is there code for X?

[Scott Morrison]

I need to prove

example (x : Int) : x % 2 = 0 ∨ x % 2 = 1 := by sorry

but only using Std. Any hints?

[Timo Carlin-Burns]

One way would be to have docs#Nat.mod_lt and then do cases x % 2 twice

[Scott Morrison]

That would work nicely for Nat, but not for Int.

[Scott Morrison]

Ah, but

example (x : Int) : x % 2 = 0 ∨ x % 2 = 1 := by
  have h₁ := Int.emod_nonneg x (b := 2) (by decide)
  have h₂ := Int.emod_lt_of_pos x (b := 2) (by decide)
  match x % 2, h₁, h₂ with
  | 0, _, _ => simp
  | 1, _, _ => simp

does it.

[Scott Morrison]

Thanks.