Definition padicapart : apart commringofpadicints. Proof. intros. split with padicapart1. split. - unfold padicapart1. apply ( isirreflquotrel padicapartiscomprel isirreflpadicapart0 ). - split. + apply ( issymmquotrel padicapartiscomprel issymmpadicapart0 ). + apply ( iscotransquotrel padicapartiscomprel iscotranspadicapart0 ). 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.