Definition gcdisgreatest ( n m : hz ) ( i : hzneq 0 n ): ∏ l : hz, iscommonhzdiv l n m → hzleh l (gcd n m i) := pr2 ( pr2 ( pr1 ( euclideanalgorithm n m i ) ) ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.