let n, k be non zero Nat; :: thesis: for g being Element of (INT.Group n) st g = k holds
g " = (n - k) mod n
let g be Element of (INT.Group n); :: thesis: ( g = k implies g " = (n - k) mod n )
assume A1: g = k ; :: thesis: g " = (n - k) mod n
A2: ( k in Segm n & (n - k) mod n in Segm n )

proof

k in INT.Group n by A1;
hence k in Segm n by Th76; :: thesis: (n - k) mod n in Segm n
B1: 0 <= (n - k) mod n by INT_1:57;
B2: (n - k) mod n < n by INT_1:58;
(n - k) mod n in NAT by B1, INT_1:3;
hence (n - k) mod n in Segm n by B2, NAT_1:44; :: thesis: verum

end;

then reconsider g2 = (n - k) mod n as Element of (INT.Group n) by Th76;
A3: n - k in NAT

proof

k < n by A2, NAT_1:44;
then 0 < n - k by XREAL_1:50;
hence n - k in NAT by INT_1:3; :: thesis: verum

end;

g * g2 = (addint n) . (k,((n - k) mod n)) by A1, Th75
.= (k + ((n - k) mod n)) mod n by A2, GR_CY_1:def 4
.= (k + (n - k)) mod n by A3, NAT_D:23
.= 0 by INT_1:50
.= 1_ (INT.Group n) by GR_CY_1:14 ;
then g " = g2 by GROUP_1:5;
hence g " = (n - k) mod n ; :: thesis: verum