Lemma hzqrandtimeseq ( m : hz ) ( x : hzneq 0 m ) ( a b : hz ) : ( a * b ) = ( ( m * ( ( 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 ) ) ) ) + hzremaindermod m x ( hzremaindermod m x a * hzremaindermod m x b ) ). Proof. intros. rewrite 3! hzldistr. rewrite ( hzplusassoc _ _ ( hzremaindermod m x ( hzremaindermod m x a * hzremaindermod m x b ) ) ). rewrite <- hzdivequationmod. rewrite ( hzmultassoc _ _ m ). rewrite <- ( hzmultassoc m _ ( hzquotientmod m x b * m ) ). rewrite ( hzmultcomm _ m ). change ( ((m * hzquotientmod m x a * (m * hzquotientmod m x b))%hz + m * (hzremaindermod m x b * hzquotientmod m x a)%hz)%ring ) with ((m * hzquotientmod m x a * (m * hzquotientmod m x b)) + m * (hzremaindermod m x b * hzquotientmod m x a) )%hz. change ( a * b = (((m * hzquotientmod m x a * (m * hzquotientmod m x b) + m * (hzremaindermod m x b * hzquotientmod m x a))%hz + m * (hzremaindermod m x a * hzquotientmod m x b)%hz)%ring + hzremaindermod m x a * hzremaindermod m x b) ) with ( a * b = (((m * hzquotientmod m x a * (m * hzquotientmod m x b) + m * (hzremaindermod m x b * hzquotientmod m x a)) + m * (hzremaindermod m x a * hzquotientmod m x b))%hz + hzremaindermod m x a * hzremaindermod m x b) ). rewrite ( hzplusassoc ( m * hzquotientmod m x a * ( m * hzquotientmod m x b ) ) _ _ ). rewrite ( hzpluscomm ( m * ( hzremaindermod m x b * hzquotientmod m x a ) ) ( m * ( hzremaindermod m x a * hzquotientmod m x b ) ) ). rewrite <- ( hzmultassoc m ( hzremaindermod m x a ) ( hzquotientmod m x b ) ). rewrite ( hzmultcomm m ( hzremaindermod m x a ) ). rewrite ( hzmultassoc ( hzremaindermod m x a ) m ( hzquotientmod m x b ) ). rewrite <- ( hzplusassoc ( m * hzquotientmod m x a * ( m * hzquotientmod m x b ) ) ( hzremaindermod m x a * ( m * hzquotientmod m x b ) ) _ ). rewrite <- hzrdistr. rewrite <- hzdivequationmod. rewrite hzplusassoc. rewrite ( hzmultcomm ( hzremaindermod m x b ) ( hzquotientmod m x a ) ). rewrite <- ( hzmultassoc m ( hzquotientmod m x a ) ( hzremaindermod m x b ) ). rewrite <- hzrdistr. rewrite <- hzdivequationmod. rewrite <- hzldistr. rewrite <- hzdivequationmod. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.