Lemma hzqrandpluseq ( p : hz ) ( x : hzneq 0 p ) ( a c : hz ) : ( a + c ) = ( ( p * ( hzquotientmod p x a + hzquotientmod p x c + hzquotientmod p x ( hzremaindermod p x a + hzremaindermod p x c ) ) ) + hzremaindermod p x ( ( hzremaindermod p x a ) + ( hzremaindermod p x c ) ) ). Proof. intros. rewrite 2! hzldistr. rewrite hzplusassoc. rewrite <- ( hzdivequationmod p x ( hzremaindermod p x a + hzremaindermod p x c ) ). rewrite hzplusassoc. rewrite ( hzpluscomm ( hzremaindermod p x a ) ). rewrite <- ( hzplusassoc ( p * hzquotientmod p x c ) ). rewrite <- ( hzdivequationmod p x c ). rewrite ( hzpluscomm c ). rewrite <- hzplusassoc. rewrite <- ( hzdivequationmod p x a ). apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.