Lemma carryandzero : carry p ( isaprimetoneq0 is ) 0 = 0. Proof. intros. unfold carry. rewrite precarryandzero. assert ( forall n : nat, (fun n : nat => hzremaindermod p (isaprimetoneq0 is) ( @ringunel1 ( fpscommring hz ) n)) n = @ringunel1 ( fpscommring hz ) n ) as f. { intros n. rewrite hzqrand0r. unfold carry. change ( @ringunel1 ( fpscommring hz) n ) with 0%hz. apply idpath. } apply ( funextfun _ _ f ). 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.