Lemma hzqrandnatsummation0r ( m : hz ) ( x : hzneq 0 m ) ( a : nat -> hz ) ( upper : nat ) : hzremaindermod m x ( natsummation0 upper a ) = hzremaindermod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) ). Proof. intros. induction upper. - simpl. rewrite hzremaindermoditerated. apply idpath. - change ( hzremaindermod m x ( natsummation0 upper a + a ( S upper ) ) = hzremaindermod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) + hzremaindermod m x ( a ( S upper ) ) ) ). rewrite hzremaindermodandplus. rewrite IHupper. rewrite <- ( hzremaindermoditerated m x ( a ( S upper ) ) ). rewrite <- hzremaindermodandplus. rewrite hzremaindermoditerated. 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.