proposition: Lemma divandhzabsval ( n : hz ) : hzdiv n ( nattohz ( hzabsval n ) ).
proof: 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.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble