:: deftheorem Def2 defines idiv_prgPRGCOR_1:def 2 : for n, m, b3 being Integer holds ( b3=idiv_prg (n,m) iff ex i being Integer st ( ( m =0 implies b3=0 ) & ( not m =0 implies ( ( n >=0 & m >0 implies b3=idiv1_prg (n,m) ) & ( ( not n >=0 or not m >0 ) implies ( ( n >=0 & m <0 implies ( i =idiv1_prg (n,(- m)) & ( (- m)* i = n implies b3=- i ) & ( (- m)* i <> n implies b3=(- i)- 1 ) ) ) & ( ( not n >=0 or not m <0 ) implies ( ( n <0 & m >0 implies ( i =idiv1_prg ((- n),m) & ( m * i =- n implies b3=- i ) & ( m * i <>- n implies b3=(- i)- 1 ) ) ) & ( ( not n <0 or not m >0 ) implies b3=idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) );