Lemma ringcarryequiv : @ringeqrel ( fpscommring hz ). Proof. intros. split with carryequiv. split. - split. + intros a b c q. simpl. simpl in q. rewrite carryandplus. rewrite q. rewrite <- carryandplus. apply idpath. + intros a b c q. simpl. rewrite carryandplus. rewrite q. rewrite <- carryandplus. apply idpath. - split. + intros a b c q. simpl. rewrite carryandtimes. rewrite q. rewrite <- carryandtimes. apply idpath. + intros a b c q. simpl. rewrite carryandtimes. rewrite q. rewrite <- carryandtimes. 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.