Lemma hzgcdandminusr ( m n : hz ) : hzgcd m n = hzgcd m ( - n ). Proof. intros. rewrite 2! ( hzgcdsymm m ). rewrite hzgcdandminusl. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.