Lemma hzquotientmodandtimes ( m : hz ) ( x : hzneq 0 m ) ( a b : hz ) : hzquotientmod 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 ) ) ). Proof. intros. apply pathsinv0. apply ( hzqrtestq m x ( a * b ) _ ( hzremaindermod m x ( hzremaindermod m x a * hzremaindermod m x b ) ) ). split. - apply hzqrandtimeseq. - apply hzqrandtimesineq. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.