let n be Nat; :: thesis: ( n > 0 implies for a, b being Element of Segm n holds

( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) ) )

assume A1: n > 0 ; :: thesis: for a, b being Element of Segm n holds

( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) )

let a, b be Element of Segm n; :: thesis: ( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) )

reconsider n = n as non zero Nat by A1;

consider c being Element of NAT such that

A2: c = (a + b) mod n ;

consider t being Nat such that

A3: ( ( a + b = (n * t) + c & c < n ) or ( c = 0 & n = 0 ) ) by A2, NAT_D:def 2;

( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) ) )

assume A1: n > 0 ; :: thesis: for a, b being Element of Segm n holds

( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) )

let a, b be Element of Segm n; :: thesis: ( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) )

reconsider n = n as non zero Nat by A1;

consider c being Element of NAT such that

A2: c = (a + b) mod n ;

consider t being Nat such that

A3: ( ( a + b = (n * t) + c & c < n ) or ( c = 0 & n = 0 ) ) by A2, NAT_D:def 2;

A4: now :: thesis: ( a + b >= n implies (addint n) . (a,b) = (a + b) - n )

A9:
( (addint n) . (a,b) = (a + b) - n implies a + b >= n )
assume A5:
a + b >= n
; :: thesis: (addint n) . (a,b) = (a + b) - n

t = 1

end;t = 1

proof

end;

hence
(addint n) . (a,b) = (a + b) - n
by A2, A3, GR_CY_1:def 4; :: thesis: verumnow :: thesis: ( ( t = 0 & t = 1 ) or ( t <> 0 & t = 1 ) )end;

hence
t = 1
; :: thesis: verumper cases
( t = 0 or t <> 0 )
;

end;

case A6:
t <> 0
; :: thesis: t = 1

t < 2

then A8: t <= 1 by NAT_1:13;

1 + 0 <= t by A6, INT_1:7;

hence t = 1 by A8, XXREAL_0:1; :: thesis: verum

end;proof

then
t < 1 + 1
;
( a < n & b < n )
by NAT_1:44;

then A7: ( (n * t) + c >= n * t & a + b < (n * 1) + (n * 1) ) by NAT_1:11, XREAL_1:8;

assume t >= 2 ; :: thesis: contradiction

then n * t >= n * 2 by XREAL_1:64;

hence contradiction by A3, A7, XXREAL_0:2; :: thesis: verum

end;then A7: ( (n * t) + c >= n * t & a + b < (n * 1) + (n * 1) ) by NAT_1:11, XREAL_1:8;

assume t >= 2 ; :: thesis: contradiction

then n * t >= n * 2 by XREAL_1:64;

hence contradiction by A3, A7, XXREAL_0:2; :: thesis: verum

then A8: t <= 1 by NAT_1:13;

1 + 0 <= t by A6, INT_1:7;

hence t = 1 by A8, XXREAL_0:1; :: thesis: verum

proof

assume
(addint n) . (a,b) = (a + b) - n
; :: thesis: a + b >= n

then A10: (a + b) mod n = (a + b) - n by GR_CY_1:def 4;

consider t being Nat such that

A11: a + b = (n * t) + ((a + b) mod n) and

(a + b) mod n < n by NAT_D:def 2;

assume A12: a + b < n ; :: thesis: contradiction

t = 0

end;then A10: (a + b) mod n = (a + b) - n by GR_CY_1:def 4;

consider t being Nat such that

A11: a + b = (n * t) + ((a + b) mod n) and

(a + b) mod n < n by NAT_D:def 2;

assume A12: a + b < n ; :: thesis: contradiction

t = 0

proof

hence
contradiction
by A10, A11; :: thesis: verum
assume
t <> 0
; :: thesis: contradiction

then 1 + 0 <= t by INT_1:7;

then A13: 1 * n <= t * n by XREAL_1:64;

t * n <= (t * n) + ((a + b) mod n) by NAT_1:11;

hence contradiction by A12, A11, A13, XXREAL_0:2; :: thesis: verum

end;then 1 + 0 <= t by INT_1:7;

then A13: 1 * n <= t * n by XREAL_1:64;

t * n <= (t * n) + ((a + b) mod n) by NAT_1:11;

hence contradiction by A12, A11, A13, XXREAL_0:2; :: thesis: verum

A14: now :: thesis: ( a + b < n implies (addint n) . (a,b) = a + b )

( (addint n) . (a,b) = a + b implies a + b < n )
assume A15:
a + b < n
; :: thesis: (addint n) . (a,b) = a + b

t = 0

end;t = 0

proof

hence
(addint n) . (a,b) = a + b
by A2, A3, GR_CY_1:def 4; :: thesis: verum
assume
t <> 0
; :: thesis: contradiction

then 1 + 0 <= t by INT_1:7;

then A16: 1 * n <= t * n by XREAL_1:64;

n * t <= (n * t) + c by NAT_1:11;

hence contradiction by A3, A15, A16, XXREAL_0:2; :: thesis: verum

end;then 1 + 0 <= t by INT_1:7;

then A16: 1 * n <= t * n by XREAL_1:64;

n * t <= (n * t) + c by NAT_1:11;

hence contradiction by A3, A15, A16, XXREAL_0:2; :: thesis: verum

proof

hence
( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) )
by A14, A9, A4; :: thesis: verum
assume
(addint n) . (a,b) = a + b
; :: thesis: a + b < n

then (a + b) mod n = a + b by GR_CY_1:def 4;

hence a + b < n by NAT_D:1; :: thesis: verum

end;then (a + b) mod n = a + b by GR_CY_1:def 4;

hence a + b < n by NAT_D:1; :: thesis: verum