:: deftheorem Def11 defines compint INT_3:def 11 :
for n being natural Number st n > 0 holds
for b₂ being UnOp of (Segm n) holds
( b₂ = compint n iff for k being Element of Segm n holds b₂ . k = (n - k) mod n );