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