proposition: Lemma hzqrand1eq ( p : hz ) ( is : isaprime p ) : 1 = ( ( p * 0 ) + 1 ).
proof: Proof. intros. rewrite hzmultx0. rewrite hzplusl0. apply idpath. Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble