Lemma hzabsvalandminuspos ( n m : hz ) ( p : hzleh 0 n ) ( q : hzleh 0 m ) : nattohz ( hzabsval ( n - m ) ) = nattohz ( hzabsval ( m - n ) ). Proof. intros. destruct ( hzlthorgeh n m ) as [ l | r ]. - assert ( hzlth ( n - m ) 0 ) as a. { change ( n - m ) with ( n + - m ). rewrite <- ( hzrminus m ). change ( m - m ) with ( m + - m ). apply hzlthandplusr. assumption. } assert ( hzlth 0 ( m - n ) ) as b. { change ( m - n ) with ( m + - n ). rewrite <- ( hzrminus n ). change ( n - n ) with ( n + - n ). apply hzlthandplusr. assumption. } rewrite ( hzabsvallth0 a ). rewrite hzabsvalgth0. + change ( n - m ) with ( n + - m ). rewrite hzaddinvplus. change ( - - m ) with ( - - m )%ring. rewrite ringminusminus. rewrite hzpluscomm. apply idpath. + apply b. - destruct ( hzgehchoice n m r ) as [ h | k ]. + assert ( hzlth 0 ( n - m ) ) as a. { change ( n - m ) with ( n + - m ). rewrite <- ( hzrminus m ). change ( m - m ) with ( m + - m ). apply hzlthandplusr. assumption. } assert ( hzlth ( m - n ) 0 ) as b. { change ( m - n ) with ( m + - n ). rewrite <- ( hzrminus n ). apply hzlthandplusr. apply h. } rewrite ( hzabsvallth0 b ). rewrite hzabsvalgth0. * change ( n + - m = - ( m + - n ) ). rewrite hzaddinvplus. change ( - - n ) with ( - - n )%ring. rewrite ringminusminus. rewrite hzpluscomm. apply idpath. * apply a. + rewrite k. apply idpath. 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.