Definition padicapart0 : hrel ( fpscommring hz ) := fun a b => ∃ n : nat, neq _ ( carry p ( isaprimetoneq0 is) a n ) ( carry p ( isaprimetoneq0 is) b n ).
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.