proposition: Lemma primedivorcoprime ( a : hz ) : hzdiv p a ∨ gcd p a ( isaprimetoneq0 is ) = 1.
proof: Proof. intros P i. use (hinhuniv _ ( pr2 is ( gcd p a ( isaprimetoneq0 is ) ) ( pr1 ( gcdiscommondiv p a ( isaprimetoneq0 is ) ) ) )). intro t. apply i. destruct t as [ t0 | t1 ]. - apply ii2. assumption. - apply ii1. rewrite <- t1. exact ( pr2 ( gcdiscommondiv p a ( isaprimetoneq0 is ) ) ). Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers