theorem :: NUMBER16:15

( 4,11 are_coprime & ( for m being Nat holds not (ArProg (4,11)) . m is Fibonacci ) )