let m, k, l be Nat; :: thesis: ( k <> l & 1 <= k & k <= m & 1 <= l & l <= m implies ((m !) * k) + 1,((m !) * l) + 1 are_coprime )
assume S1: ( k <> l & 1 <= k & k <= m & 1 <= l & l <= m ) ; :: thesis: ((m !) * k) + 1,((m !) * l) + 1 are_coprime
assume not ((m !) * k) + 1,((m !) * l) + 1 are_coprime ; :: thesis: contradiction
then consider d being non zero Nat such that
A1: ( d <> 1 & d divides ((m !) * k) + 1 & d divides ((m !) * l) + 1 ) by MOEBIUS2:5;

per cases ( k < l or k > l ) by S1, XXREAL_0:1;

suppose k < l ; :: thesis: contradiction

then b1: l - k > k - k by XREAL_1:14;
a1: d divides l * (((m !) * k) + 1) by A1, NAT_D:9;
d divides k * (((m !) * l) + 1) by A1, NAT_D:9;
then A2: d divides (l * (((m !) * k) + 1)) - (k * (((m !) * l) + 1)) by a1, PREPOWER:94;
A3: l - k <= m - k by S1, XREAL_1:13;
m - k < m by S1, XREAL_1:44;
then A5: l - k < m by A3, XXREAL_0:2;
d <= l - k by b1, A2, NAT_D:7;
then d <= m by A5, XXREAL_0:2;
then d divides (m !) * k by NAT_D:9, NEWTON:41;
hence contradiction by A1, WSIERP_1:15, NAT_D:10; :: thesis: verum

end;

suppose k > l ; :: thesis: contradiction

then b1: k - l > l - l by XREAL_1:14;
a1: d divides l * (((m !) * k) + 1) by A1, NAT_D:9;
d divides k * (((m !) * l) + 1) by A1, NAT_D:9;
then A2: d divides (k * (((m !) * l) + 1)) - (l * (((m !) * k) + 1)) by a1, PREPOWER:94;
A3: k - l <= m - l by S1, XREAL_1:13;
m - l < m by S1, XREAL_1:44;
then A5: k - l < m by A3, XXREAL_0:2;
d <= k - l by b1, A2, NAT_D:7;
then d <= m by A5, XXREAL_0:2;
then d divides (m !) * k by NAT_D:9, NEWTON:41;
hence contradiction by A1, WSIERP_1:15, NAT_D:10; :: thesis: verum

end;

end;