proposition: Lemma hzmultr1 ( x : hz ) : ( x * 1 ) = x .
proof: Proof. Proof . apply ( ringrunax2 _ x ) . Defined . Lemma hzmultl1 ( x : hz ) : ( 1 * x ) = x . Proof . apply ( ringlunax2 _ x ) . Defined . Lemma hzmult0x ( x : hz ) : ( 0 * x ) = 0 . Proof . apply ( ringmult0x _ x ) . Defined . Lemma hzmultx0 ( x : hz ) : ( x * 0 ) = 0 . Proof . apply ( ringmultx0 _ x ) . Defined . Lemma hzmultassoc ( x y z : hz ) : ( ( x * y ) * z ) = ( x * ( y * z ) ) . Proof . intros . apply ( ringassoc2 hz x y z ) . Defined . Lemma hzmultcomm ( x y : hz ) : ( x * y ) = ( y * x ) . Proof . intros . apply ( ringcomm2 hz x y ) . Defined . Definition hzneq0andmultlinv ( n m : hz ) ( isnm : hzneq ( n * m ) 0 ) : hzneq n 0 := ringneq0andmultlinv hz n m isnm . Definition hzneq0andmultrinv ( n m : hz ) ( isnm : hzneq ( n * m ) 0 ) : hzneq m 0 := ringneq0andmultrinv hz n m isnm . Definition hzgth : hrel hz := rigtoringrel natcommrig isplushrelnatgth . Definition hzlth : hrel hz := λ a b, hzgth b a . Definition hzleh : hrel hz := λ a b, make_hProp ( neg ( hzgth a b ) ) ( isapropneg _ ) . Definition hzgeh : hrel hz := λ a b, make_hProp ( neg ( hzgth b a ) ) ( isapropneg _ ) . Lemma isdecrelhzgth : isdecrel hzgth . Proof . apply ( isdecrigtoringrel natcommrig isplushrelnatgth ) . apply isinvplushrelnatgth . apply isdecrelnatgth . Defined . Definition hzgthdec := make_decrel isdecrelhzgth . Definition isdecrelhzlth : isdecrel hzlth := λ x x', isdecrelhzgth x' x . Definition hzlthdec := make_decrel isdecrelhzlth . Definition isdecrelhzleh : isdecrel hzleh := isdecnegrel _ isdecrelhzgth . Definition hzlehdec := make_decrel isdecrelhzleh . Definition isdecrelhzgeh : isdecrel hzgeh := λ x x', isdecrelhzleh x' x . Definition hzgehdec := make_decrel isdecrelhzgeh . Lemma istranshzgth ( n m k : hz ) : hzgth n m -> hzgth m k -> hzgth n k . Proof. apply ( istransabgrdiffrel nataddabmonoid isplushrelnatgth ) . unfold istrans . apply istransnatgth . Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra