m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ ((Even (m - n) ↔ Even n) ↔ Even n)
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Even m ↔ Even n)
conv_rhs => rw [← tsub_add_cancel_of_le h, even_add]
no goals
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ ((Even (m - n) ↔ Even n) ↔ Even n)
by_cases h : Even n <;> simp [h]