Division algorithms for norm-Euclidean real quadratic fields -- part I

We give a Euclidean division algorithm for the real quadratic fields $\mathbb{Q}(\sqrt{m})$ for $m\in \{2,3,6,7,11,19\}$, with the property that the norm of the remainder depends on the first Euclidean minimum of the field. In each case, we cover the square $[-1\mathrm{/}2,1\mathrm{/}2]\times [-1\mathrm{/}2,1\mathrm{/}2]$ with hyperbolas and give a list of these, together with regions covered. We mechanize the proofs as much as we can, using exact computations, in order to be able to reproduce them.