fact: Definition padicapart0 : hrel ( fpscommring hz ) := fun a b => ∃ n : nat, neq _ ( carry p ( isaprimetoneq0 is) a n ) ( carry p ( isaprimetoneq0 is) b n ).
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers