-- Consecutive Fibonacci numbers are coprime, and so are Fibonacci numbers
-- two apart
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.NumberTheory.FibonacciGCD
import GCDMore
import Combinatorics.Fibonacci

theorem fibonacci.coprime_consecutive (n : Nat)
  shows gcd(fibonacci(n), fibonacci(n + 1)) = 1
proof
  induction n
  | zero =>
    have zero := fibonacci.zero
    have index : fibonacci(0 + 1) = 1
      have sum : 0 + 1 = 1 by ring
      rw sum
      exact fibonacci.one
    rw [zero, index]
    exact gcd.zero_left at 1
  | k + 1 using ih =>
    have two : k + 1 + 1 = k + 2 by ring
    have step := fibonacci.succ_succ at k
    rw [two, step]
    have shifted := gcd.add_right_swap at fibonacci(k + 1), fibonacci(k)
    rw shifted
    have commute := gcd.commutative at fibonacci(k + 1), fibonacci(k)
    rw commute
    exact ih

theorem fibonacci.coprime_consecutive_left (n : Nat)
  shows gcd(fibonacci(n + 1), fibonacci(n)) = 1
proof
  have commute := gcd.commutative at fibonacci(n + 1), fibonacci(n)
  rw commute
  exact fibonacci.coprime_consecutive at n

theorem fibonacci.coprime_skip (n : Nat)
  shows gcd(fibonacci(n), fibonacci(n + 2)) = 1
proof
  have step := fibonacci.succ_succ at n
  rw step
  have shifted := gcd.add_right at fibonacci(n), fibonacci(n + 1)
  rw shifted
  exact fibonacci.coprime_consecutive at n

theorem fibonacci.divides_consecutive_one (d n : Nat)
  requires left : d ∣ fibonacci(n)
  requires right : d ∣ fibonacci(n + 1)
  shows d = 1
proof
  have coprimeFib := fibonacci.coprime_consecutive at n
  exact coprime.divisor_one at fibonacci(n), fibonacci(n + 1), d
    with coprimeFib, left, right