Fixpoint precarry ( a : fpscommring hz ) ( n : nat ) : hz := match n with | 0%nat => a 0%nat | S n => a ( S n ) + hzquotientmod m is ( precarry a n ) end.
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.