let n be non empty Nat; :: thesis: for m being Nat st m <> 1 & m divides Fib n holds
not m divides Fib (n -' 1)
A1: n >= 1 by NAT_2:21;
let m be Nat; :: thesis: ( m <> 1 & m divides Fib n implies not m divides Fib (n -' 1) )
assume A2: m <> 1 ; :: thesis: ( not m divides Fib n or not m divides Fib (n -' 1) )
assume A3: m divides Fib n ; :: thesis: not m divides Fib (n -' 1)
assume A4: m divides Fib (n -' 1) ; :: thesis: contradiction
n = (n -' 1) + 1 by A1, XREAL_1:237;
then Fib (n -' 1), Fib n are_relative_prime by Th69;
then (Fib (n -' 1)) gcd (Fib n) = 1 by INT_2:def 4;
then m divides 1 by A3, A4, NAT_D:def 5;
hence contradiction by A2, WSIERP_1:20; :: thesis: verum