Lemma divandhzabsval ( n : hz ) : hzdiv n ( nattohz ( hzabsval n ) ). Proof. intros. destruct ( hzlthorgeh 0 n ) as [ left | right ]. - intros P s. apply s. split with 1. unfold hzdiv0. rewrite hzmultr1. rewrite hzabsvalgth0. + apply idpath. + assumption. - intros P s. apply s. split with ( - 1%hz ). unfold hzdiv0. rewrite ( ringrmultminus hz ). rewrite hzmultr1. rewrite hzabsvalleh0. + apply idpath. + assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.