Lemma gcdneq0 ( n m : hz ) ( i : hzneq 0 n ) : hzneq 0 ( gcd n m i ). Proof. intros. intro f. apply ( nozerodiv n ). - assumption. - rewrite f. exact ( pr1 ( gcdiscommondiv n m i ) ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.