Theorem: Misc.Nat.even_iff (LeanSAT/Util/Misc.lean)

State before:
n : Nat
x✝ : Even n
m : Nat
hm : n = m + m
⊢ n % 2 = 0
Tactic:
simp only [hm, ← Nat.two_mul, Nat.mul_mod_right]
State after:
no goals

State before:
n : Nat
h : n % 2 = 0
⊢ n % 2 + 2 * (n / 2) = n / 2 + n / 2
Tactic:
simp only [h, Nat.zero_add, Nat.two_mul]
State after:
no goals