let a, b, c, d be Nat; :: thesis: ( a,b are_coprime & a + b divides (a * c) + (b * d) implies a + b divides c - d )
assume A1: ( a,b are_coprime & a + b divides (a * c) + (b * d) ) ; :: thesis: a + b divides c - d
set u = a * c;
set v = - (b * d);
A1a: a + b divides (a * c) - (- (b * d)) by A1;
A2: a + b divides (a * ((a * c) + 0)) + (b * ((- (b * d)) + 0)) by A1a, Th31;
consider t being Integer such that
A4: ((a * a) * c) - ((b * b) * d) = (a + b) * t by A2;
A6: (a * b) * (c - d) = (((a * c) - (b * d)) - t) * (a + b) by A4;
( a,a + b are_coprime & b,a + b are_coprime ) by A1, EULER_1:7;
then a * b,a + b are_coprime by WSIERP_1:6;
hence a + b divides c - d by A6, INT_1:def 3, WSIERP_1:29; :: thesis: verum