Lemma hzqrandnatsummation0q ( m : hz ) ( x : hzneq 0 m ) ( a : nat -> hz ) ( upper : nat ) : hzquotientmod m x ( natsummation0 upper a ) = ( natsummation0 upper ( fun n : nat => hzquotientmod m x ( a n ) ) + hzquotientmod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) ) ). Proof. intros. induction upper. - simpl. rewrite <- hzqrandremainderq. rewrite hzplusr0. apply idpath. - change ( natsummation0 ( S upper ) a ) with ( natsummation0 upper a + a ( S upper ) ). rewrite hzquotientmodandplus. rewrite IHupper. rewrite ( hzplusassoc ( natsummation0 upper ( fun n : nat => hzquotientmod m x ( a n ) ) ) _ ( hzquotientmod m x ( a ( S upper ) ) ) ). rewrite ( hzpluscomm ( hzquotientmod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) ) ) ( hzquotientmod m x ( a ( S upper ) ) ) ). rewrite <- ( hzplusassoc ( natsummation0 upper ( fun n : nat => hzquotientmod m x ( a n ) ) ) ( hzquotientmod m x ( a ( S upper ) ) ) _ ). change ( natsummation0 upper ( fun n : nat => hzquotientmod m x ( a n ) ) + hzquotientmod m x ( a ( S upper ) ) ) with ( natsummation0 ( S upper ) ( fun n : nat => hzquotientmod m x ( a n ) ) ). rewrite hzqrandnatsummation0r. rewrite hzquotientmodandplus. rewrite <- hzqrandremainderq. rewrite hzplusl0. rewrite hzremaindermoditerated. rewrite ( hzplusassoc (natsummation0 ( S upper ) ( fun n : nat => hzquotientmod m x ( a n ) ) ) ( hzquotientmod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) ) ) _ ). rewrite <- ( hzplusassoc ( hzquotientmod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) ) ) _ _ ). rewrite <- hzquotientmodandplus. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.PAdics.fps. Require Import UniMath.PAdics.frac. Require Import UniMath.PAdics.z_mod_p. Require Import UniMath.NumberSystems.Integers.