Lemma padicapartcomputation ( a b : fpscommring hz ) : ( pr1 padicapart ) ( setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) a ) ( setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) b ) = padicapart0 a b. Proof. intros. apply hPropUnivalence. - intros i. apply i. - intro u. apply u. 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.