Lemma isaprophzgcd ( n m : hz ) : isaprop ( hzgcd n m ). Proof. intros. intros k l. assert ( isofhlevel 2 ( hzgcd n m ) ) as aux. { apply isofhleveltotal2. - apply isasethz. - intros x. apply hlevelntosn. apply isofhleveldirprod. + apply isapropiscommonhzdiv. + apply impred. intro t. apply impredfun. apply ( hzleh t x ). } assert ( k = l ) as f. { destruct k as [ k pq ]. destruct pq as [ p q ]. destruct l as [ l pq ]. destruct pq as [ p' q' ]. assert ( k = l ) as f0. { apply isantisymmhzleh. - apply q'. assumption. - apply q. assumption. } apply ( total2_paths2_f f0 ). assert ( isaprop ( iscommonhzdiv l n m × forall x : hz, iscommonhzdiv x n m -> hzleh x l ) ) as is. { apply isofhleveldirprod. - apply isapropiscommonhzdiv. - apply impred. intro t. apply impredfun. apply ( hzleh t l ). } apply is. } split with f. intro g. destruct k as [ k pq ]. destruct pq as [ p q ]. destruct l as [ l pq ]. destruct pq as [ p' q' ]. apply aux. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.