Lemma issymmpadicapart0 : issymm padicapart0. Proof. intros a b f. use (hinhuniv _ f). intros u. destruct u as [ n u ]. apply total2tohexists. split with n. intros g. unfold neq in u. apply u. rewrite g. apply idpath. 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.