Definition acommringofpadicints : acommring. Proof. intros. split with commringofpadicints. split with padicapart. split. - split. + apply padicplusisbinopapartl. + apply padicplusisbinopapartr. - split. + apply padictimesisbinopapartl. + apply padictimesisbinopapartr. 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.