proposition: Lemma hzabsvalchoice ( n : hz ) : ( 0%nat = hzabsval n ) ⨿ ( ∑ x : nat, S x = hzabsval n ).
proof: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids