proposition: 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: 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.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers