proposition: Lemma isirreflpadicapart0 : isirrefl padicapart0.
proof: 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.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers