Definition hzgcd ( n m : hz ) : UU := ∑ k : hz, iscommonhzdiv k n m × forall l : hz, iscommonhzdiv l n m -> hzleh l k.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.