Lemma hzremaindermodandmultl ( p : hz ) ( x : hzneq 0 p ) ( a b : hz ) : hzremaindermod p x ( p * a + b ) = hzremaindermod p x b. Proof. intros. assert ( p * a + b = ( p * ( a + hzquotientmod p x b ) + hzremaindermod p x b ) ) as f. { rewrite hzldistr. rewrite hzplusassoc. rewrite <- ( hzdivequationmod p x b ). apply idpath. } rewrite hzremaindermodandplus. rewrite hzremaindermodandtimes. rewrite hzqrandselfr. rewrite hzmult0x. rewrite hzqrand0r. rewrite hzplusl0. rewrite hzremaindermoditerated. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.