let a, b be Nat; :: thesis: ( a < b & b <> 0 implies (2 * a) div b < 2 )
assume A1: a < b ; :: thesis: ( not b <> 0 or (2 * a) div b < 2 )
assume A2: b <> 0 ; :: thesis: (2 * a) div b < 2

per cases ( 2 * a < b or 2 * a >= b ) ;

suppose 2 * a < b ; :: thesis: (2 * a) div b < 2

then (2 * a) div b = 0 by NAT_D:27;
hence (2 * a) div b < 2 ; :: thesis: verum

end;

suppose 2 * a >= b ; :: thesis: (2 * a) div b < 2

then (2 * a) - b >= b - b by XREAL_1:13;
then (2 * a) - b >= 0 ;
then (2 * a) - b in NAT by INT_1:3;
then reconsider ab = (2 * a) - b as Nat ;
A4: b div b = (b * 1) div b
.= 1 by A2, NAT_D:18 ;
A5: b mod b = (b * 1) mod b
.= 0 by NAT_D:13 ;
2 * a < 2 * b by A1, XREAL_1:68;
then (2 * a) - b < (2 * b) - b by XREAL_1:9;
then A6: ab div b = 0 by NAT_D:27;
(2 * a) div b = (ab + b) div b
.= (ab div b) + (b div b) by A5, NAT_D:19
.= 1 by A4, A6 ;
hence (2 * a) div b < 2 ; :: thesis: verum

end;

end;