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