let a, b, n, k be Nat; :: thesis: ( b > 0 & k > 0 & a + b > k & a + b divides k * (a |^ n) implies not a,b are_coprime )
assume A1: ( b > 0 & k > 0 & a + b > k & a + b divides k * (a |^ n) ) ; :: thesis: not a,b are_coprime
defpred S₁[ Nat] means ( a + b divides k * (a |^ $1) implies not a,b are_coprime );
L1: S₁[ 0 ]

proof

k * (a |^ 0) = k * 1 by NEWTON:4;
hence S₁[ 0 ] by A1, INT_2:27; :: thesis: verum

end;

L2: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
assume B1: S₁[x] ; :: thesis: S₁[x + 1]
B2: a |^ (x + 1) = (a |^ x) * a by NEWTON:6;
( a,b are_coprime & not a + b divides k * (a |^ x) implies not a + b divides k * (a |^ (x + 1)) )

proof

assume C1: ( a,b are_coprime & not a + b divides k * (a |^ x) ) ; :: thesis: not a + b divides k * (a |^ (x + 1))
then 1 = (b + (1 * a)) gcd a by A1, EULER_1:16;
then a + b,a are_coprime ;
then not a + b divides (k * (a |^ x)) * a by C1, INT_2:25;
hence not a + b divides k * (a |^ (x + 1)) by B2; :: thesis: verum

end;

hence S₁[x + 1] by B1; :: thesis: verum

end;

for c being Nat holds S₁[c] from NAT_1:sch 2(L1, L2);
hence not a,b are_coprime by A1; :: thesis: verum