let k, n be Element of NAT ; :: thesis: ( n > 1 & k <> 0 & k <> 1 implies ( Fib k = Fib n iff k = n ) )
assume that
A1: n > 1 and
A2: ( k <> 0 & k <> 1 ) ; :: thesis: ( Fib k = Fib n iff k = n )
not k is trivial by A2, NAT_2:def 1;
then k >= 1 + 1 by NAT_2:29;
then A3: k > 1 by NAT_1:13;
( Fib k = Fib n implies k = n )
proof
assume A4: Fib k = Fib n ; :: thesis: k = n
assume A5: k <> n ; :: thesis: contradiction
per cases ( k > n or k < n ) by A5, XXREAL_0:1;
end;
end;
hence ( Fib k = Fib n iff k = n ) ; :: thesis: verum