Lemma gcdand0 ( n : hz ) ( i : hzneq 0 n ) : ( gcd n 0 i = n ) ⨿ ( gcd n 0 i = - n ). Proof. intros. apply gcdanddiv. apply hzdivand0. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.