Lemma gcdandprime ( p : hz ) ( x : hzneq 0 p ) ( y : isaprime p ) ( a : hz ) ( q : neg ( hzmod p x a 0 ) ) : gcd p a x = 1. Proof. intros. assert ( isaprop ( gcd p a x = 1) ) as is by apply isasethz. apply ( pr2 y ( gcd p a x ) ( pr1 ( gcdiscommondiv p a x ) ) (make_hProp _ is ) ). intro t. destruct t as [ t0 | t1 ]. - apply t0. - apply fromempty. apply q. simpl. assert ( hzremaindermod p x a = 0 ) as f. { assert ( hzdiv p a ) as u. { rewrite <- t1. apply ( pr2 ( gcdiscommondiv _ _ _ ) ). } rewrite hzremaindermodanddiv. + apply idpath. + assumption. } rewrite f. rewrite hzqrand0r. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.