Lemma hzquotientandtimesl ( m : hz ) ( x : hzneq 0 m ) ( a b : hz ) : hzquotientmod m x ( a * b ) = ( hzquotientmod m x a ) * b + hzremaindermod m x a * hzquotientmod m x b + hzquotientmod m x ( hzremaindermod m x a * hzremaindermod m x b ). Proof. intros. rewrite hzquotientmodandtimes. rewrite ( hzmultcomm ( hzremaindermod m x b ) ( hzquotientmod m x a ) ). rewrite hzmultassoc. rewrite <- ( hzldistr ( hzquotientmod m x b * m ) _ ( hzquotientmod m x a )). rewrite ( hzmultcomm _ m ). rewrite <- ( hzdivequationmod m x b ). rewrite hzplusassoc. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.PAdics.fps. Require Import UniMath.PAdics.frac. Require Import UniMath.PAdics.z_mod_p. Require Import UniMath.NumberSystems.Integers.