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