Lemma carryequiviseqrel : iseqrel carryequiv0. Proof. split. - split. + intros a b c i j. simpl. rewrite i. apply j. + intros a. simpl. apply idpath. - intros a b i. simpl. rewrite i. 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.