proposition: Lemma hzmodiseqrel ( p : hz ) ( x : hzneq 0 p ) : iseqrel ( hzmod p x ).
proof: Proof. intros. apply iseqrelconstr. - exact ( hzmodistrans p x ). - exact ( hzmodisrefl p x ). - exact ( hzmodissymm p x ). Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble