let a, b be odd Integer; :: thesis: ( a mod b is odd iff a div b is even )
thus ( a mod b is odd implies a div b is even ) :: thesis: ( a div b is even implies a mod b is odd )

proof

assume a mod b is odd ; :: thesis: a div b is even
then a - ((a div b) * b) is odd by INT_1:def 10;
hence a div b is even ; :: thesis: verum

end;

assume a div b is even ; :: thesis: a mod b is odd
then a - ((a div b) * b) is odd ;
hence a mod b is odd by INT_1:def 10; :: thesis: verum