proposition: Lemma hzremaindermodandtimes ( m : hz ) ( x : hzneq 0 m ) ( a b : hz ) : hzremaindermod m x ( a * b ) = ( hzremaindermod m x ( hzremaindermod m x a * hzremaindermod m x b ) ).
proof: Proof. intros. apply pathsinv0. apply ( hzqrtestr m x ( a * b ) ( ( hzquotientmod m x ) a * ( hzquotientmod m x ) b * m + ( hzremaindermod m x b ) * ( hzquotientmod m x a ) + ( hzremaindermod m x a ) * ( hzquotientmod m x b ) + ( hzquotientmod m x ( hzremaindermod m x a * hzremaindermod m x b ) ) ) _ ). split. - apply hzqrandtimeseq. - apply hzqrandtimesineq. Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble