Definition gcdiscommondiv ( n m : hz ) ( i : hzneq 0 n ) : iscommonhzdiv (gcd n m i) n m := pr1 ( pr2 ( pr1 ( euclideanalgorithm n m i ) ) ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.