Definition hzqrtestr ( m : hz ) ( x : hzneq 0 m ) ( a q r : hz ) ( d : a = ( m * q ) + r × ( hzleh 0 r × hzlth r ( nattohz ( hzabsval m ) ) ) ) := pr2 ( hzqrtest m x a q r d ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.