Lemma hzremaindermodanddiv ( p : hz ) ( x : hzneq 0 p ) ( a : hz ) ( y : hzdiv p a ) : hzremaindermod p x a = 0. Proof. intros. assert ( isaprop ( hzremaindermod p x a = 0 ) ) as v by apply isasethz. apply ( y ( make_hProp _ v ) ). intro t. destruct t as [ k f ]. unfold hzdiv0 in f. assert ( a = p * k + 0 ) as f'. { rewrite f. rewrite hzplusr0. apply idpath. } set ( e := tpair ( P := (fun qr : hz × hz => a = p * pr1 qr + pr2 qr × ( hzleh 0 (pr2 qr) × hzlth (pr2 qr) (nattohz (hzabsval p)))) ) ( make_dirprod k 0 ) (make_dirprod f' ( make_dirprod ( isreflhzleh 0 ) ( lemmas.hzabsvalneq0 p x ) ) ) ). assert ( e = pr1 ( divalgorithm a p x ) ) as s by apply ( pr2 ( divalgorithm a p x ) ). set ( w := base_paths _ _ ( pathsinv0 s ) ). unfold e in w. unfold hzremaindermod. apply ( maponpaths ( fun z : hz × hz => pr2 z ) w ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.