proposition: Lemma hzlthlehtrans ( n m k : hz ) : hzlth n m -> hzleh m k -> hzlth n k .
proof: Proof. Proof . intros l1 l2 . apply ( hzgehgthtrans k m n l2 l1 ) . Defined . Lemma hzlehlthtrans ( n m k : hz ) : hzleh n m -> hzlth m k -> hzlth n k . Proof . intros l1 l2 . apply ( hzgthgehtrans k m n l2 l1 ) . Defined . Definition hzgthandplusl ( n m k : hz ) : hzgth n m -> hzgth ( k + n ) ( k + m ) . Proof. apply ( pr1 ( isbinopabgrdiffrel nataddabmonoid isplushrelnatgth ) ) . Defined . Definition hzgthandplusr ( n m k : hz ) : hzgth n m -> hzgth ( n + k ) ( m + k ) . Proof. apply ( pr2 ( isbinopabgrdiffrel nataddabmonoid isplushrelnatgth ) ) . Defined . Definition hzgthandpluslinv ( n m k : hz ) : hzgth ( k + n ) ( k + m ) -> hzgth n m . Proof. intros g . set ( g' := hzgthandplusl _ _ ( - k ) g ) . clearbody g' . rewrite ( pathsinv0 ( hzplusassoc _ _ n ) ) in g' . rewrite ( pathsinv0 ( hzplusassoc _ _ m ) ) in g' . rewrite ( hzlminus k ) in g' . rewrite ( hzplusl0 _ ) in g' . rewrite ( hzplusl0 _ ) in g' . apply g' . Defined . Definition hzgthandplusrinv ( n m k : hz ) : hzgth ( n + k ) ( m + k ) -> hzgth n m . Proof. intros l . rewrite ( hzpluscomm n k ) in l . rewrite ( hzpluscomm m k ) in l . apply ( hzgthandpluslinv _ _ _ l ) . Defined . Lemma hzgthsnn ( n : hz ) : hzgth ( n + 1 ) n . Proof . set ( int := hzgthandplusl _ _ n ( ct ( hzgth , isdecrelhzgth, 1 , 0 ) ) ) . clearbody int . rewrite ( hzplusr0 _ ) in int . apply int . Defined . Definition hzlthandplusl ( n m k : hz ) : hzlth n m -> hzlth ( k + n ) ( k + m ) := hzgthandplusl _ _ _ . Definition hzlthandplusr ( n m k : hz ) : hzlth n m -> hzlth ( n + k ) ( m + k ) := hzgthandplusr _ _ _ . Definition hzlthandpluslinv ( n m k : hz ) : hzlth ( k + n ) ( k + m ) -> hzlth n m := hzgthandpluslinv _ _ _ . Definition hzlthandplusrinv ( n m k : hz ) : hzlth ( n + k ) ( m + k ) -> hzlth n m := hzgthandplusrinv _ _ _ . Definition hzlthnsn ( n : hz ) : hzlth n ( n + 1 ) := hzgthsnn n . Definition hzlehandplusl ( n m k : hz ) : hzleh n m -> hzleh ( k + n ) ( k + m ) := negf ( hzgthandpluslinv n m k ) . Definition hzlehandplusr ( n m k : hz ) : hzleh n m -> hzleh ( n + k ) ( m + k ) := negf ( hzgthandplusrinv n m k ) . Definition hzlehandpluslinv ( n m k : hz ) : hzleh ( k + n ) ( k + m ) -> hzleh n m := negf ( hzgthandplusl n m k ) . Definition hzlehandplusrinv ( n m k : hz ) : hzleh ( n + k ) ( m + k ) -> hzleh n m := negf ( hzgthandplusr n m k ) . Definition hzgehandplusl ( n m k : hz ) : hzgeh n m -> hzgeh ( k + n ) ( k + m ) := negf ( hzgthandpluslinv m n k ) . Definition hzgehandplusr ( n m k : hz ) : hzgeh n m -> hzgeh ( n + k ) ( m + k ) := negf ( hzgthandplusrinv m n k ) . Definition hzgehandpluslinv ( n m k : hz ) : hzgeh ( k + n ) ( k + m ) -> hzgeh n m := negf ( hzgthandplusl m n k ) . Definition hzgehandplusrinv ( n m k : hz ) : hzgeh ( n + k ) ( m + k ) -> hzgeh n m := negf ( hzgthandplusr m n k ) . Lemma isplushrelhzgth : @isbinophrel hzaddabgr hzgth . Proof . split . apply hzgthandplusl . apply hzgthandplusr . Defined . Lemma isinvplushrelhzgth : @isinvbinophrel hzaddabgr hzgth . Proof . split . apply hzgthandpluslinv . apply hzgthandplusrinv . Defined . Lemma isringmulthzgth : isringmultgt _ hzgth . Proof . apply ( isringrigtoringmultgt natcommrig isplushrelnatgth isrigmultgtnatgth ) . Defined . Lemma isinvringmulthzgth : isinvringmultgt _ hzgth . Proof . apply ( isinvringrigtoringmultgt natcommrig isplushrelnatgth isinvplushrelnatgth isinvrigmultgtnatgth ) . Defined . Lemma hzgth0andminus { n : hz } ( is : hzgth n 0 ) : hzlth ( - n ) 0 . Proof . intros . apply ( ringfromgt0 hz isplushrelhzgth ) . apply is . Defined . Lemma hzminusandgth0 { n : hz } ( is : hzgth ( - n ) 0 ) : hzlth n 0 . Proof . intros . apply ( ringtolt0 hz isplushrelhzgth ) . apply is . Defined . Lemma hzlth0andminus { n : hz } ( is : hzlth n 0 ) : hzgth ( - n ) 0 . Proof . intros . apply ( ringfromlt0 hz isplushrelhzgth ) . apply is . Defined . Lemma hzminusandlth0 { n : hz } ( is : hzlth ( - n ) 0 ) : hzgth n 0 . Proof . intros . apply ( ringtogt0 hz isplushrelhzgth ) . apply is . Defined . Lemma hzleh0andminus { n : hz } ( is : hzleh n 0 ) : hzgeh ( - n ) 0 . Proof . revert is. apply ( negf ( @hzminusandlth0 n ) ) . Defined . Lemma hzminusandleh0 { n : hz } ( is : hzleh ( - n ) 0 ) : hzgeh n 0 . Proof . revert is. apply ( negf ( @hzlth0andminus n ) ) . Defined . Lemma hzgeh0andminus { n : hz } ( is : hzgeh n 0 ) : hzleh ( - n ) 0 . Proof . revert is . apply ( negf ( @hzminusandgth0 n ) ) . Defined . Lemma hzminusandgeh0 { n : hz } ( is : hzgeh ( - n ) 0 ) : hzleh n 0 . Proof . revert is . apply ( negf ( @hzgth0andminus n ) ) . Defined . Definition hzgthandmultl ( n m k : hz ) ( is : hzgth k hzzero ) : hzgth n m -> hzgth ( k * n ) ( k * m ) . Proof. revert n m k is. apply ( isringmultgttoislringmultgt _ isplushrelhzgth isringmulthzgth ) . Defined . Definition hzgthandmultr ( n m k : hz ) ( is : hzgth k hzzero ) : hzgth n m -> hzgth ( n * k ) ( m * k ) . Proof . revert n m k is. apply ( isringmultgttoisrringmultgt _ isplushrelhzgth isringmulthzgth ) . Defined . Definition hzgthandmultlinv ( n m k : hz ) ( is : hzgth k hzzero ) : hzgth ( k * n ) ( k * m ) -> hzgth n m . Proof . intros is' . apply ( isinvringmultgttoislinvringmultgt hz isplushrelhzgth isinvringmulthzgth n m k is is' ) . Defined . Definition hzgthandmultrinv ( n m k : hz ) ( is : hzgth k hzzero ) : hzgth ( n * k ) ( m * k ) -> hzgth n m . Proof. intros is' . apply ( isinvringmultgttoisrinvringmultgt hz isplushrelhzgth isinvringmulthzgth n m k is is' ) . Defined . Definition hzlthandmultl ( n m k : hz ) ( is : hzgth k 0 ) : hzlth n m -> hzlth ( k * n ) ( k * m ) := hzgthandmultl _ _ _ is . Definition hzlthandmultr ( n m k : hz ) ( is : hzgth k 0 ) : hzlth n m -> hzlth ( n * k ) ( m * k ) := hzgthandmultr _ _ _ is . Definition hzlthandmultlinv ( n m k : hz ) ( is : hzgth k 0 ) : hzlth ( k * n ) ( k * m ) -> hzlth n m := hzgthandmultlinv _ _ _ is . Definition hzlthandmultrinv ( n m k : hz ) ( is : hzgth k 0 ) : hzlth ( n * k ) ( m * k ) -> hzlth n m := hzgthandmultrinv _ _ _ is . Definition hzlehandmultl ( n m k : hz ) ( is : hzgth k 0 ) : hzleh n m -> hzleh ( k * n ) ( k * m ) := negf ( hzgthandmultlinv _ _ _ is ) . Definition hzlehandmultr ( n m k : hz ) ( is : hzgth k 0 ) : hzleh n m -> hzleh ( n * k ) ( m * k ) := negf ( hzgthandmultrinv _ _ _ is ) . Definition hzlehandmultlinv ( n m k : hz ) ( is : hzgth k 0 ) : hzleh ( k * n ) ( k * m ) -> hzleh n m := negf ( hzgthandmultl _ _ _ is ) . Definition hzlehandmultrinv ( n m k : hz ) ( is : hzgth k 0 ) : hzleh ( n * k ) ( m * k ) -> hzleh n m := negf ( hzgthandmultr _ _ _ is ) . Definition hzgehandmultl ( n m k : hz ) ( is : hzgth k 0 ) : hzgeh n m -> hzgeh ( k * n ) ( k * m ) := negf ( hzgthandmultlinv _ _ _ is ) . Definition hzgehandmultr ( n m k : hz ) ( is : hzgth k 0 ) : hzgeh n m -> hzgeh ( n * k ) ( m * k ) := negf ( hzgthandmultrinv _ _ _ is ) . Definition hzgehandmultlinv ( n m k : hz ) ( is : hzgth k 0 ) : hzgeh ( k * n ) ( k * m ) -> hzgeh n m := negf ( hzgthandmultl _ _ _ is ) . Definition hzgehandmultrinv ( n m k : hz ) ( is : hzgth k 0 ) : hzgeh ( n * k ) ( m * k ) -> hzgeh n m := negf ( hzgthandmultr _ _ _ is ) . Lemma hzmultgth0gth0 { m n : hz } ( ism : hzgth m 0 ) ( isn : hzgth n 0 ) : hzgth ( m * n ) 0 . Proof . intros . apply isringmulthzgth . apply ism . apply isn . Defined . Lemma hzmultgth0geh0 { m n : hz } ( ism : hzgth m 0 ) ( isn : hzgeh n 0 ) : hzgeh ( m * n ) 0 . Proof . intros . destruct ( hzgehchoice _ _ isn ) as [ gn | en ] . apply ( hzgthtogeh _ _ ( hzmultgth0gth0 ism gn ) ) . rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh . Defined . Lemma hzmultgeh0gth0 { m n : hz } ( ism : hzgeh m 0 ) ( isn : hzgth n 0 ) : hzgeh ( m * n ) 0 . Proof . intros . destruct ( hzgehchoice _ _ ism ) as [ gm | em ] . apply ( hzgthtogeh _ _ ( hzmultgth0gth0 gm isn ) ) . rewrite em . rewrite ( hzmult0x _ ) . apply isreflhzgeh . Defined . Lemma hzmultgeh0geh0 { m n : hz } ( ism : hzgeh m 0 ) ( isn : hzgeh n 0 ) : hzgeh ( m * n ) 0 . Proof . intros . destruct ( hzgehchoice _ _ isn ) as [ gn | en ] . apply ( hzmultgeh0gth0 ism gn ) . rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh . Defined . Lemma hzmultgth0lth0 { m n : hz } ( ism : hzgth m 0 ) ( isn : hzlth n 0 ) : hzlth ( m * n ) 0 . Proof . intros . apply ( ringmultgt0lt0 hz isplushrelhzgth isringmulthzgth ) . apply ism . apply isn . Defined . Lemma hzmultgth0leh0 { m n : hz } ( ism : hzgth m 0 ) ( isn : hzleh n 0 ) : hzleh ( m * n ) 0 . Proof . intros . destruct ( hzlehchoice _ _ isn ) as [ ln | en ] . apply ( hzlthtoleh _ _ ( hzmultgth0lth0 ism ln ) ) . rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzleh . Defined . Lemma hzmultgeh0lth0 { m n : hz } ( ism : hzgeh m 0 ) ( isn : hzlth n 0 ) : hzleh ( m * n ) 0 . Proof . intros . destruct ( hzlehchoice _ _ ism ) as [ lm | em ] . apply ( hzlthtoleh _ _ ( hzmultgth0lth0 lm isn ) ) . destruct em . rewrite ( hzmult0x _ ) . apply isreflhzleh . Defined . Lemma hzmultgeh0leh0 { m n : hz } ( ism : hzgeh m 0 ) ( isn : hzleh n 0 ) : hzleh ( m * n ) 0 . Proof . intros . destruct ( hzlehchoice _ _ isn ) as [ ln | en ] . apply ( hzmultgeh0lth0 ism ln ) . rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzleh . Defined . Lemma hzmultlth0gth0 { m n : hz } ( ism : hzlth m 0 ) ( isn : hzgth n 0 ) : hzlth ( m * n ) 0 . Proof . intros . rewrite ( hzmultcomm ) . apply hzmultgth0lth0 . apply isn . apply ism . Defined . Lemma hzmultlth0geh0 { m n : hz } ( ism : hzlth m 0 ) ( isn : hzgeh n 0 ) : hzleh ( m * n ) 0 . Proof . intros . rewrite ( hzmultcomm ) . apply hzmultgeh0lth0 . apply isn . apply ism . Defined . Lemma hzmultleh0gth0 { m n : hz } ( ism : hzleh m 0 ) ( isn : hzgth n 0 ) : hzleh ( m * n ) 0 . Proof . intros . rewrite ( hzmultcomm ) . apply hzmultgth0leh0 . apply isn . apply ism . Defined . Lemma hzmultleh0geh0 { m n : hz } ( ism : hzleh m 0 ) ( isn : hzgeh n 0 ) : hzleh ( m * n ) 0 . Proof . intros . rewrite ( hzmultcomm ) . apply hzmultgeh0leh0 . apply isn . apply ism . Defined . Lemma hzmultlth0lth0 { m n : hz } ( ism : hzlth m 0 ) ( isn : hzlth n 0 ) : hzgth ( m * n ) 0 . Proof . intros . assert ( ism' := hzlth0andminus ism ) . assert ( isn' := hzlth0andminus isn ) . assert ( int := isringmulthzgth _ _ ism' isn' ) . rewrite ( ringmultminusminus hz ) in int . apply int . Defined . Lemma hzmultlth0leh0 { m n : hz } ( ism : hzlth m 0 ) ( isn : hzleh n 0 ) : hzgeh ( m * n ) 0 . Proof . intros . intros . destruct ( hzlehchoice _ _ isn ) as [ ln | en ] . apply ( hzgthtogeh _ _ ( hzmultlth0lth0 ism ln ) ) . rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh . Defined . Lemma hzmultleh0lth0 { m n : hz } ( ism : hzleh m 0 ) ( isn : hzlth n 0 ) : hzgeh ( m * n ) 0 . Proof . intros . destruct ( hzlehchoice _ _ ism ) as [ lm | em ] . apply ( hzgthtogeh _ _ ( hzmultlth0lth0 lm isn ) ) . rewrite em . rewrite ( hzmult0x _ ) . apply isreflhzgeh . Defined . Lemma hzmultleh0leh0 { m n : hz } ( ism : hzleh m 0 ) ( isn : hzleh n 0 ) : hzgeh ( m * n ) 0 . Proof . intros . destruct ( hzlehchoice _ _ isn ) as [ ln | en ] . apply ( hzmultleh0lth0 ism ln ) . rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh . Defined . Lemma isintdomhz : isintdom hz . Proof . split with isnonzerorighz . intros a b e0 . destruct ( isdeceqhz a 0 ) as [ ea | nea ] . apply ( hinhpr ( ii1 ea ) ) . destruct ( isdeceqhz b 0 ) as [ eb | neb ] . apply ( hinhpr ( ii2 eb ) ) . destruct ( hzneqchoice _ _ nea ) as [ ga | la ] . destruct ( hzneqchoice _ _ neb ) as [ gb | lb ] . destruct ( hzgthtoneq _ _ ( hzmultgth0gth0 ga gb ) e0 ) . destruct ( hzlthtoneq _ _ ( hzmultgth0lth0 ga lb ) e0 ) . destruct ( hzneqchoice _ _ neb ) as [ gb | lb ] . destruct ( hzlthtoneq _ _ ( hzmultlth0gth0 la gb ) e0 ) . destruct ( hzgthtoneq _ _ ( hzmultlth0lth0 la lb ) e0 ) . Defined . Definition hzintdom : intdom := tpair _ _ isintdomhz . Definition hzneq0andmult ( n m : hz ) ( isn : hzneq n 0 ) ( ism : hzneq m 0 ) : hzneq ( n * m ) 0 := intdomneq0andmult hzintdom n m isn ism . Lemma hzmultlcan ( a b c : hz ) ( ne : neg ( c = 0 ) ) ( e : ( c * a ) = ( c * b ) ) : a = b . Proof . intros . apply ( intdomlcan hzintdom _ _ _ ne e ) . Defined . Lemma hzmultrcan ( a b c : hz ) ( ne : neg ( c = 0 ) ) ( e : ( a * c ) = ( b * c ) ) : a = b . Proof . intros . apply ( intdomrcan hzintdom _ _ _ ne e ) . Defined . Lemma isinclhzmultl ( n : hz )( ne : neg ( n = 0 ) ) : isincl ( λ m : hz, n * m ) . Proof. intros . apply ( pr1 ( intdomiscancelable hzintdom n ne ) ) . Defined . Lemma isinclhzmultr ( n : hz )( ne : neg ( n = 0 ) ) : isincl ( λ m : hz, m * n ) . Proof. intros . apply ( pr2 ( intdomiscancelable hzintdom n ne ) ) . Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra