Definition padicintegers : aintdom. Proof. intros. split with acommringofpadicints. split. - change ( pr1 padicapart padicone padiczero ). rewrite padiczerocomputation. rewrite padiconecomputation. rewrite padicapartcomputation. apply total2tohexists. split with 0%nat. unfold carry. unfold precarry. rewrite hzqrand1r. rewrite hzqrand0r. apply isnonzerorighz. - apply padicintsareintdom. 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.