If your algorithm does not at all depend on the result of division, you can replace it by a constant parameter Div(_,_). For theorem proving, you should then be able to prove the properties that you are interested in. For model checking, you will still need to provide an instance of that operator, say
Div(x,y) == 42
but you can run TLC with different definitions to become confident that the definition is indeed irrelevant. However, if this is true, it sounds like you could write an even more abstract specification, such as getting rid of variables to which division is applied.
If your algorithm depends on certain properties of division but not the precise result you can state those in an ASSUME clause, say,
ASSUME \A x,y \in Int : y # 0 => Div(x,y) \in Int /\ Div(x,y) < x
Stephan