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