let l, p, n1, n2 be Nat; :: thesis: ( 0 <> l & p > l & p > n1 & p > n2 & (l * n1) mod p = (l * n2) mod p & p is prime implies n1 = n2 )
assume that
A1: ( l <> 0 & p > l ) and
A2: p > n1 and
A3: p > n2 ; :: thesis: ( not (l * n1) mod p = (l * n2) mod p or not p is prime or n1 = n2 )
assume A4: (l * n1) mod p = (l * n2) mod p ; :: thesis: ( not p is prime or n1 = n2 )
assume A5: p is prime ; :: thesis: n1 = n2
then ((l * n1) - (l * n2)) mod p = 0 by A4, INT_4:22;
then A6: p divides l * (n1 - n2) by A5, INT_1:62;

per cases ( p divides l or p divides n1 - n2 ) by A5, A6, INT_5:7;

suppose p divides l ; :: thesis: n1 = n2

hence n1 = n2 by A1, NAT_D:7; :: thesis: verum

end;

suppose A7: p divides n1 - n2 ; :: thesis: n1 = n2

per cases ( n1 - n2 > 0 or n1 - n2 = 0 or n1 - n2 < 0 ) ;

suppose A8: n1 - n2 > 0 ; :: thesis: n1 = n2

then ( p divides n1 -' n2 & n1 -' n2 > 0 ) by A7, XREAL_0:def 2;
then p <= n1 -' n2 by NAT_D:7;
then p + n2 <= (n1 -' n2) + n2 by XREAL_1:6;
then p + n2 <= (n1 - n2) + n2 by A8, XREAL_0:def 2;
then p + n2 < p by A2, XXREAL_0:2;
then (p + n2) - p < p - p by XREAL_1:9;
then n2 < 0 ;
hence n1 = n2 ; :: thesis: verum

end;

suppose n1 - n2 = 0 ; :: thesis: n1 = n2

hence n1 = n2 ; :: thesis: verum

end;

suppose n1 - n2 < 0 ; :: thesis: n1 = n2

then A9: - (n1 - n2) > 0 ;
then A10: n2 - n1 > 0 ;
then A11: n2 -' n1 > 0 by XREAL_0:def 2;
p divides - (n1 - n2) by A7, INT_2:10;
then p divides n2 -' n1 by A10, XREAL_0:def 2;
then p <= n2 -' n1 by A11, NAT_D:7;
then p + n1 <= (n2 -' n1) + n1 by XREAL_1:6;
then p + n1 <= (n2 - n1) + n1 by A9, XREAL_0:def 2;
then p + n1 < p by A3, XXREAL_0:2;
then (p + n1) - p < p - p by XREAL_1:9;
then n1 < 0 ;
hence n1 = n2 ; :: thesis: verum

end;

end;

end;

end;