Lemma isirreflpadicapart0 : isirrefl padicapart0. Proof. intros a f. simpl in f. assert hfalse as x. { apply f. intros u. destruct u as [ n u ]. apply u. apply idpath. } exact x. 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.