let n, m be Integer; :: thesis: for n2, m2 being Element of NAT holds ( ( m =0 & n2 = n & m2 = m implies ( n div m =0 & n2 div m2 =0 ) ) & ( n >=0 & m >0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >=0 & m <0 & n2 = n & m2 =- m implies ( ( m2 *(n2 div m2)= n2 implies n div m =-(n2 div m2) ) & ( m2 *(n2 div m2)<> n2 implies n div m =(-(n2 div m2))- 1 ) ) ) & ( n <0 & m >0 & n2 =- n & m2 = m implies ( ( m2 *(n2 div m2)= n2 implies n div m =-(n2 div m2) ) & ( m2 *(n2 div m2)<> n2 implies n div m =(-(n2 div m2))- 1 ) ) ) & ( n <0 & m <0 & n2 =- n & m2 =- m implies n div m = n2 div m2 ) ) let n2, m2 be Element of NAT ; :: thesis: ( ( m =0 & n2 = n & m2 = m implies ( n div m =0 & n2 div m2 =0 ) ) & ( n >=0 & m >0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >=0 & m <0 & n2 = n & m2 =- m implies ( ( m2 *(n2 div m2)= n2 implies n div m =-(n2 div m2) ) & ( m2 *(n2 div m2)<> n2 implies n div m =(-(n2 div m2))- 1 ) ) ) & ( n <0 & m >0 & n2 =- n & m2 = m implies ( ( m2 *(n2 div m2)= n2 implies n div m =-(n2 div m2) ) & ( m2 *(n2 div m2)<> n2 implies n div m =(-(n2 div m2))- 1 ) ) ) & ( n <0 & m <0 & n2 =- n & m2 =- m implies n div m = n2 div m2 ) ) thus
( m =0 & n2 = n & m2 = m implies ( n div m =0 & n2 div m2 =0 ) )
byINT_1:48; :: thesis: ( ( n >=0 & m >0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >=0 & m <0 & n2 = n & m2 =- m implies ( ( m2 *(n2 div m2)= n2 implies n div m =-(n2 div m2) ) & ( m2 *(n2 div m2)<> n2 implies n div m =(-(n2 div m2))- 1 ) ) ) & ( n <0 & m >0 & n2 =- n & m2 = m implies ( ( m2 *(n2 div m2)= n2 implies n div m =-(n2 div m2) ) & ( m2 *(n2 div m2)<> n2 implies n div m =(-(n2 div m2))- 1 ) ) ) & ( n <0 & m <0 & n2 =- n & m2 =- m implies n div m = n2 div m2 ) ) thus
( n >=0 & m >0 & n2 = n & m2 = m implies n div m = n2 div m2 )
; :: thesis: ( ( n >=0 & m <0 & n2 = n & m2 =- m implies ( ( m2 *(n2 div m2)= n2 implies n div m =-(n2 div m2) ) & ( m2 *(n2 div m2)<> n2 implies n div m =(-(n2 div m2))- 1 ) ) ) & ( n <0 & m >0 & n2 =- n & m2 = m implies ( ( m2 *(n2 div m2)= n2 implies n div m =-(n2 div m2) ) & ( m2 *(n2 div m2)<> n2 implies n div m =(-(n2 div m2))- 1 ) ) ) & ( n <0 & m <0 & n2 =- n & m2 =- m implies n div m = n2 div m2 ) ) thus
( n >=0 & m <0 & n2 = n & m2 =- m implies ( ( m2 *(n2 div m2)= n2 implies n div m =-(n2 div m2) ) & ( m2 *(n2 div m2)<> n2 implies n div m =(-(n2 div m2))- 1 ) ) )
:: thesis: ( ( n <0 & m >0 & n2 =- n & m2 = m implies ( ( m2 *(n2 div m2)= n2 implies n div m =-(n2 div m2) ) & ( m2 *(n2 div m2)<> n2 implies n div m =(-(n2 div m2))- 1 ) ) ) & ( n <0 & m <0 & n2 =- n & m2 =- m implies n div m = n2 div m2 ) )