proposition: Lemma quotientandtimesrearrangel ( x y : hz ) : hzquotientmod m is ( x * y ) = ( hzquotientmod m is x ) * y + hzquotientmod m is ( ( hzremaindermod m is x ) * y ).
proof: Proof. intros. rewrite hzquotientmodandtimes. change (hzquotientmod m is x * hzquotientmod m is y * m + hzremaindermod m is y * hzquotientmod m is x + hzremaindermod m is x * hzquotientmod m is y + hzquotientmod m is (hzremaindermod m is x * hzremaindermod m is y))%hz with (hzquotientmod m is x * hzquotientmod m is y * m + hzremaindermod m is y * hzquotientmod m is x + hzremaindermod m is x * hzquotientmod m is y + hzquotientmod m is (hzremaindermod m is x * hzremaindermod m is y))%ring. rewrite ( ringcomm2 hz ( hzremaindermod m is y ) ( hzquotientmod m is x ) ). rewrite ( ringassoc2 hz ). rewrite <- ( ringldistr hz ). rewrite ( ringcomm2 hz ( hzquotientmod m is y ) m ). change (m * hzquotientmod m is y + hzremaindermod m is y)%ring with (m * hzquotientmod m is y + hzremaindermod m is y)%hz. rewrite <- ( hzdivequationmod m is y ). change (hzremaindermod m is x * y)%ring with (hzremaindermod m is x * y)%hz. rewrite ( hzquotientmodandtimes m is ( hzremaindermod m is x ) y ). rewrite hzremaindermoditerated. rewrite <- hzqrandremainderq. rewrite hzmultx0. rewrite 2! hzmult0x. rewrite hzplusl0. rewrite ( ringassoc1 hz ). change (hzquotientmod m is x * y + (hzremaindermod m is x * hzquotientmod m is y + hzquotientmod m is (hzremaindermod m is x * hzremaindermod m is y))%hz) with (hzquotientmod m is x * y + (hzremaindermod m is x * hzquotientmod m is y + hzquotientmod m is (hzremaindermod m is x * hzremaindermod m is y)))%ring. apply idpath. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers