Lemma primedivorcoprime ( a : hz ) : hzdiv p a ∨ gcd p a ( isaprimetoneq0 is ) = 1. 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.
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.