Lemma isaprophzgcd0 ( k n m : hz ) : isaprop ( iscommonhzdiv k n m × forall l : hz, iscommonhzdiv l n m -> hzleh l k ). Proof. intros. apply isofhleveldirprod. - apply isapropiscommonhzdiv. - apply impred. intro t. apply impredfun. apply hzleh. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.