Lemma hzdivisrefl : isrefl hzdiv. Proof. red. intro. unfold hzdiv. apply total2tohexists. split with 1. apply hzmultr1. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.