proposition: 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: 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.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers