In the context of an abstract formalisation of division with remainder in an interactive theorem prover, I came upon the following problem: The following two properties seem rather natural for a division with remainder (for $b\neq 0$ and $c\neq 0$):
$$(a + c \cdot b)\ \mathrm{div}\ b = c + a\ \mathrm{div}\ b$$ $$(c \cdot a)\ \mathrm{div}\ (c \cdot b) = a\ \mathrm{div}\ b$$
Let's assume that we have a Euclidean domain. I was unable to prove that these properties hold for any division operation that fulfils the requirements of a Euclidean domain. (and I suspect that this is simply not true, although I haven't found a counterexample either)
My question is: What additional properties – ideally few, simple, and natural ones – do I have to assume to prove these two facts? Is there perhaps a standard algebraic structure where these hold?
I know of uniquely Euclidean norms and I think the properties should be relatively easy to infer in those. However, a number of interesting rings fulfil the two conditions I gave above, but they are not uniquely Euclidean: integers and, (if memory serves me right) formal power series over a field.