## Stream: new members

### Topic: Frustration with simple nat lemmas

#### Eric Wieser (Nov 07 2020 at 12:27):

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,
conv_rhs { rw ←add_zero (n*n + n) },
rw add_assoc (n*n + n) n,
rw nat.add_mod_right (n + n) 2,
rw nat.zero_mod,
sorry, -- (n + n) % 2 = 0
end


#### Kevin Buzzard (Nov 07 2020 at 12:42):

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


#### Kevin Buzzard (Nov 07 2020 at 12:43):

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 (Nov 07 2020 at 12:46):

Oh, I guess I meant comm_ring R

#### Eric Wieser (Nov 07 2020 at 12:47):

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 (Nov 09 2020 at 11:13):

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?

Last updated: Dec 20 2023 at 11:08 UTC