let a, b be Integer; :: thesis: for m being Nat st (a * b) mod m = 1 & a mod m = 1 holds
b mod m = 1
let m be Nat; :: thesis: ( (a * b) mod m = 1 & a mod m = 1 implies b mod m = 1 )
assume A1: ( (a * b) mod m = 1 & a mod m = 1 ) ; :: thesis: b mod m = 1
then A2: m <> 0 by INT_1:def 10;
then a mod m = 1 mod m by A1, PEPIN:5, INT_1:58;
then a * b,1 * b are_congruent_mod m by INT_4:11, A2, NAT_D:64;
hence b mod m = 1 by A1, NAT_D:64; :: thesis: verum