Lemma hzqrtest ( m : hz ) ( x : hzneq 0 m ) ( a q r : hz ) : a = ( m * q ) + r × ( hzleh 0 r × hzlth r ( nattohz (hzabsval m ) ) ) -> q = hzquotientmod m x a × r = hzremaindermod m x a. Proof. intros d. set ( k := tpair ( P := ( fun qr : hz × hz => a = m * ( pr1 qr ) + pr2 qr × ( hzleh 0 ( pr2 qr ) × hzlth ( pr2 qr ) ( nattohz ( hzabsval m ) ) ) ) ) ( make_dirprod q r ) d ). assert ( k = pr1 ( divalgorithm a m x ) ) as f by apply ( pr2 ( divalgorithm a m x ) ). split. - change q with ( pr1 ( pr1 k ) ). rewrite f. apply idpath. - change r with ( pr2 ( pr1 k ) ). rewrite f. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.