no goals
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
⊢ xn a1 0 ≡ xn b1 0 [MOD c] ∧ yn a1 0 ≡ yn b1 0 [MOD c]
constructor <;> rfl
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
⊢ a ≡ b [MOD c] ∧ 1 ≡ 1 [MOD c]
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
⊢ xn a1 1 ≡ xn b1 1 [MOD c] ∧ yn a1 1 ≡ yn b1 1 [MOD c]
simp
no goals
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
⊢ a ≡ b [MOD c] ∧ 1 ≡ 1 [MOD c]
exact ⟨h, ModEq.refl 1⟩
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * xn a1 (n + 1) ≡ 2 * b * xn b1 (n + 1) [MOD c]
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ xn a1 (n + 2) + xn a1 n ≡ xn b1 (n + 2) + xn b1 n [MOD c]
rw [xn_succ_succ a1, xn_succ_succ b1]
no goals
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * xn a1 (n + 1) ≡ 2 * b * xn b1 (n + 1) [MOD c]
exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).left
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * b * yn b1 (n + 1) [MOD c]
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ yn a1 (n + 2) + yn (_ : 1 < a) n ≡ yn b1 (n + 2) + yn (_ : 1 < b) n [MOD c]
rw [yn_succ_succ a1, yn_succ_succ b1]
no goals
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * b * yn b1 (n + 1) [MOD c]
exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).right