Lemma padicapartiscomprel : iscomprelrel ( carryequiv p ( isaprimetoneq0 is ) ) padicapart0. Proof. intros a a' b b' i j. apply hPropUnivalence. - intro k. use (hinhuniv _ k). intros u. destruct u as [ n u ]. apply total2tohexists. split with n. rewrite <- i , <- j. assumption. - intro k. use (hinhuniv _ k). intros u. destruct u as [ n u ]. apply total2tohexists. split with n. rewrite i, j. assumption. 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.