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

proof

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

end;

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