proposition: Theorem isdeceqhz : isdeceq hz .
proof: Proof. Proof . change ( isdeceq ( abgrdiff ( rigaddabmonoid natcommrig ) ) ) . apply isdeceqabgrdiff . apply isinclnatplusr . apply isdeceqnat . Defined . Opaque isdeceqhz. Lemma isasethz : isaset hz . Proof . apply ( setproperty hzaddabgr ) . Defined . Opaque isasethz. Definition hzeq ( x y : hz ) : hProp := make_hProp ( x = y ) ( isasethz _ _ ) . Definition isdecrelhzeq : isdecrel hzeq := λ a b, isdeceqhz a b . Definition hzdeceq : decrel hz := make_decrel isdecrelhzeq . Definition hzbooleq := decreltobrel hzdeceq . Definition hzneq ( x y : hz ) : hProp := make_hProp ( neg ( x = y ) ) ( isapropneg _ ) . Definition isdecrelhzneq : isdecrel hzneq := isdecnegrel _ isdecrelhzeq . Definition hzdecneq : decrel hz := make_decrel isdecrelhzneq . Definition hzboolneq := decreltobrel hzdecneq . Local Open Scope hz_scope . Lemma isnonzerorighz : isnonzerorig hz . Proof . apply ( ct ( hzneq , isdecrelhzneq, 1 , 0 ) ) . Defined . Definition hzminuszero : ( - 0 ) = 0 := ringinvunel1 hz . Lemma hzplusr0 ( x : hz ) : ( x + 0 ) = x . Proof . apply ( ringrunax1 _ x ) . Defined . Lemma hzplusl0 ( x : hz ) : ( 0 + x ) = x . Proof . apply ( ringlunax1 _ x ) . Defined . Lemma hzplusassoc ( x y z : hz ) : ( ( x + y ) + z ) = ( x + ( y + z ) ) . Proof . intros . apply ( ringassoc1 hz x y z ) . Defined . Lemma hzpluscomm ( x y : hz ) : ( x + y ) = ( y + x ) . Proof . intros . apply ( ringcomm1 hz x y ) . Defined . Lemma hzlminus ( x : hz ) : ( -x + x ) = 0 . Proof . apply ( ringlinvax1 hz x ) . Defined . Lemma hzrminus ( x : hz ) : ( x - x ) = 0 . Proof . apply ( ringrinvax1 hz x ) . Defined . Lemma isinclhzplusr ( n : hz ) : isincl ( λ m : hz, m + n ) . Proof. apply ( pr2 ( weqtoincl ( weqrmultingr hzaddabgr n ) ) ) . Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra