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