let m be positive Nat; :: thesis: for k being Nat ex a, b being positive Nat st
( 2 * k = a - b & a,m are_coprime & b,m are_coprime )
let k be Nat; :: thesis: ex a, b being positive Nat st
( 2 * k = a - b & a,m are_coprime & b,m are_coprime )
set S = the Sierp49FS of m,k;
set q = PrimeDivisorsFS m;

per cases ( not PrimeDivisorsFS m is empty or PrimeDivisorsFS m is empty ) ;

suppose not PrimeDivisorsFS m is empty ; :: thesis: ex a, b being positive Nat st
( 2 * k = a - b & a,m are_coprime & b,m are_coprime )

then reconsider q = PrimeDivisorsFS m as CR_Sequence ;
ex a, b being positive Nat st
( 2 * k = a - b & a,m are_coprime & b,m are_coprime & a = ((CRT ( the Sierp49FS of m,k,q)) + (Product q)) + (2 * k) & b = (CRT ( the Sierp49FS of m,k,q)) + (Product q) ) by Th54;
hence ex a, b being positive Nat st
( 2 * k = a - b & a,m are_coprime & b,m are_coprime ) ; :: thesis: verum

end;

suppose PrimeDivisorsFS m is empty ; :: thesis: ex a, b being positive Nat st
( 2 * k = a - b & a,m are_coprime & b,m are_coprime )

then A1: m = 1 by Th50;
take a = (2 * k) + 2; :: thesis: ex b being positive Nat st
( 2 * k = a - b & a,m are_coprime & b,m are_coprime )
take b = 2; :: thesis: ( 2 * k = a - b & a,m are_coprime & b,m are_coprime )
thus 2 * k = a - b ; :: thesis: ( a,m are_coprime & b,m are_coprime )
thus ( a,m are_coprime & b,m are_coprime ) by A1; :: thesis: verum

end;

end;