Lemma hzabsvalchoice ( n : hz ) : ( 0%nat = hzabsval n ) ⨿ ( ∑ x : nat, S x = hzabsval n ). Proof. intros. destruct ( natlehchoice _ _ ( natleh0n ( hzabsval n ) ) ) as [ l | r ]. - apply ii2. split with ( sub ( hzabsval n ) 1 ). rewrite pathssminus. + change ( sub ( hzabsval n ) 0 = hzabsval n ). rewrite minus0r. apply idpath. + assumption. - apply ii1. assumption. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.