Lemma iscotranspadicapart0 : iscotrans padicapart0. Proof. intros a b c f. use (hinhuniv _ f). intro u. destruct u as [ n u ]. intros P j. apply j. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) a n ) ( carry p ( isaprimetoneq0 is ) b n ) ) as [ l | r ]. - apply ii2. intros Q k. apply k. split with n. intros g. unfold neq in u. apply u. rewrite l, g. apply idpath. - apply ii1. intros Q k. apply k. split with n. intros g. apply r. assumption. 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.