let a be non zero Nat; :: thesis: for b being Nat st b mod a < [/(a / 2)\] holds
(2 * b) mod a = 2 * (b mod a)
let b be Nat; :: thesis: ( b mod a < [/(a / 2)\] implies (2 * b) mod a = 2 * (b mod a) )
assume A1: b mod a < [/(a / 2)\] ; :: thesis: (2 * b) mod a = 2 * (b mod a)

per cases ( b mod a = 0 or b mod a > 0 ) ;

suppose B1: b mod a = 0 ; :: thesis: (2 * b) mod a = 2 * (b mod a)

then B2: a divides b by INT162;
b divides 2 * b ;
hence (2 * b) mod a = 2 * (b mod a) by B1, B2, INT162, INT_2:9; :: thesis: verum

end;

suppose b mod a > 0 ; :: thesis: (2 * b) mod a = 2 * (b mod a)

then a * (frac (b / a)) > 0 by R3;
then ( 0 < frac (b / a) & frac (b / a) < 1 / 2 ) by A1, MFR;
then ( 0 < 2 * (frac (b / a)) & 2 * (frac (b / a)) < 2 * (1 / 2) ) by XREAL_1:68;
then reconsider t = 2 * (frac (b / a)) as positive light Real by COMPLEX3:1;
(2 * b) mod a = a * (frac ((2 * b) / a)) by R3
.= a * (frac (2 * (b / a))) by XCMPLX_1:74
.= a * (frac (2 * (frac (b / a)))) by FR3
.= a * t
.= 2 * (a * (frac (b / a)))
.= 2 * (b mod a) by R3 ;
hence (2 * b) mod a = 2 * (b mod a) ; :: thesis: verum

end;

end;