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