Frustration with simple `nat` lemmas

Stream: new members

[Eric Wieser]

Am I missing a trick here? I can't find a lemma to close my goal, and I seem to have had to do way too much work to prove something so "obvious":

example (R : Type*) [comm_ring R] (n : ℕ) : (-1 : R) ^ ((n + 1) * (n + 1 + 1)) = (-1) ^ (n * (n + 1)) :=
begin
  conv_rhs { rw neg_one_pow_eq_pow_mod_two },
  conv_lhs { rw neg_one_pow_eq_pow_mod_two },
  congr' 1,
  simp [mul_add, add_mul],
  conv_rhs { rw ←add_zero (n*n + n) },
  rw add_assoc (n*n + n) n,
  apply nat.add_mod_eq_add_mod_left (n*n + n),
  rw [←add_assoc, ←add_assoc, add_assoc (n + n)],
  rw nat.add_mod_right (n + n) 2,
  rw nat.zero_mod,
  sorry, -- (n + n) % 2 = 0
end

[Kevin Buzzard]

example (n : ℕ) : (n + n) % 2 = 0 :=
begin
  rw ← mul_two,
  simp
end

[Kevin Buzzard]

Your example doesn't compile for me, even with adding random imports I can't make sense of (-1 : R). The way I'd prove it would to prove (1) (-1)^even=1, (2) forall t, t*(t+1) is even.

[Eric Wieser]

Oh, I guess I meant comm_ring R

[Eric Wieser]

forall t, t*(t+1) is even seems like something I've run into often enough that it would be nice if it were in mathlib

[Eric Wieser]

Ah, it's mostly there already:

example {a : ℕ} : even (a * (a + 1)) := by simp [decidable.em] with parity_simps

Is this still worth an explicit simp lemma?

@[simp]
lemma nat.even_mul_succ {a : ℕ} : even (a * (a + 1)) :=
nat.even_mul.mpr $ if h : even a then or.inl h else or.inr (nat.even_succ.mpr h)

Can we eliminate the need for writing decidable.em? Is even n ∨ ¬(even n) a good parity simp lemma?