English
gcd(fib m, fib(n+m)) = gcd(fib m, fib n).
Русский
gcd(F_m, F_{n+m}) = gcd(F_m, F_n).
LaTeX
$$gcd(fib(m), fib(n+m)) = gcd(fib(m), fib(n))$$
Lean4
theorem gcd_fib_add_self (m n : ℕ) : gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n) :=
by
rcases Nat.eq_zero_or_pos n with rfl | h
· simp
replace h := Nat.succ_pred_eq_of_pos h; rw [← h, succ_eq_add_one]
calc
gcd (fib m) (fib (n.pred + 1 + m)) = gcd (fib m) (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) :=
by
rw [← fib_add n.pred _]
ring_nf
_ = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) := by rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
_ = gcd (fib m) (fib (n.pred + 1)) :=
Coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (Coprime.symm (fib_coprime_fib_succ m))
