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