let n be non zero Nat; :: thesis: for m being Nat st m <> 1 & m divides Fib n holds
not m divides Fib (n -' 1)
let m be Nat; :: thesis: ( m <> 1 & m divides Fib n implies not m divides Fib (n -' 1) )
assume A1: m <> 1 ; :: thesis: ( not m divides Fib n or not m divides Fib (n -' 1) )
assume A2: m divides Fib n ; :: thesis: not m divides Fib (n -' 1)
n >= 1 by NAT_2:19;
then n = (n -' 1) + 1 by XREAL_1:235;
then Fib (n -' 1), Fib n are_coprime by Th67;
then A3: (Fib (n -' 1)) gcd (Fib n) = 1 by INT_2:def 3;
assume m divides Fib (n -' 1) ; :: thesis: contradiction
then m divides 1 by A2, A3, NAT_D:def 5;
hence contradiction by A1, WSIERP_1:15; :: thesis: verum