no goals
a : ℕ
a1 : 1 < a
⊢ yn a1 0 ≡ 0 [MOD 2]
simp
no goals
a : ℕ
a1 : 1 < a
⊢ yn a1 1 ≡ 1 [MOD 2]
simp
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 2 * (a * yn a1 (n + 1)) ≡ 2 * (n + 1) [MOD 2]
a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 (n + 2) + yn a1 n ≡ n + 2 + n [MOD 2]
rw [yn_succ_succ, mul_assoc, (by ring : n + 2 + n = 2 * (n + 1))]
no goals
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 2 * (a * yn a1 (n + 1)) ≡ 2 * (n + 1) [MOD 2]
exact (dvd_mul_right 2 _).modEq_zero_nat.trans (dvd_mul_right 2 _).zero_modEq_nat
no goals
a : ℕ
a1 : 1 < a
n : ℕ
⊢ n + 2 + n = 2 * (n + 1)
ring