defpred S1[ Element of NAT , Element of NAT ] means (Fib \$1) gcd (Fib \$2) = Fib (\$1 gcd \$2);
A1: for k being Element of NAT st ( for m, n being Element of NAT st m < k & n < k holds
S1[m,n] ) holds
for m being Element of NAT st m <= k holds
S1[k,m]
proof
let k be Element of NAT ; :: thesis: ( ( for m, n being Element of NAT st m < k & n < k holds
S1[m,n] ) implies for m being Element of NAT st m <= k holds
S1[k,m] )

assume A2: for m, n being Element of NAT st m < k & n < k holds
S1[m,n] ; :: thesis: for m being Element of NAT st m <= k holds
S1[k,m]

let m be Element of NAT ; :: thesis: ( m <= k implies S1[k,m] )
assume A3: m <= k ; :: thesis: S1[k,m]
per cases ( m = k or m < k ) by ;
suppose A4: m = k ; :: thesis: S1[k,m]
hence (Fib k) gcd (Fib m) = Fib k by NAT_D:32
.= Fib (k gcd m) by ;
:: thesis: verum
end;
suppose A5: m < k ; :: thesis: S1[k,m]
thus S1[k,m] :: thesis: verum
proof
per cases ( m = 0 or m > 0 ) ;
suppose A7: m > 0 ; :: thesis: S1[k,m]
thus S1[k,m] :: thesis: verum
proof
consider r being Nat such that
A8: k = m + r by ;
reconsider r = r as Element of NAT by ORDINAL1:def 12;
A9: r <= k by ;
r <> 0 by A5, A8;
then consider rr being Nat such that
A10: r = rr + 1 by NAT_1:6;
reconsider rr = rr as Element of NAT by ORDINAL1:def 12;
Fib k = ((Fib (rr + 1)) * (Fib (m + 1))) + ((Fib rr) * (Fib m)) by A8, A10, Th4;
then A11: (Fib k) gcd (Fib m) = (Fib m) gcd ((Fib (m + 1)) * (Fib r)) by ;
(Fib m) gcd (Fib (m + 1)) = 1 by Lm7;
then A12: (Fib k) gcd (Fib m) = (Fib m) gcd (Fib r) by ;
r <> k by A7, A8;
then A13: r < k by ;
k gcd m = m gcd r by ;
hence S1[k,m] by A2, A5, A12, A13; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A14: for m, n being Element of NAT st S1[m,n] holds
S1[n,m] ;
thus for m, n being Element of NAT holds S1[m,n] from :: thesis: verum