proposition: Lemma isirreflhzgth ( n : hz ) : neg ( hzgth n n ) .
proof: Proof. apply ( isirreflabgrdiffrel nataddabmonoid isplushrelnatgth ) . unfold isirrefl . apply isirreflnatgth . Defined . Lemma hzgthtoneq ( n m : hz ) ( g : hzgth n m ) : neg ( n = m ) . Proof . intros . intro e . rewrite e in g . apply ( isirreflhzgth _ g ) . Defined . Lemma isasymmhzgth ( n m : hz ) : hzgth n m -> hzgth m n -> empty . Proof. apply ( isasymmabgrdiffrel nataddabmonoid isplushrelnatgth ) . unfold isasymm . apply isasymmnatgth . Defined . Lemma isantisymmneghzgth ( n m : hz ) : neg ( hzgth n m ) -> neg ( hzgth m n ) -> n = m . Proof . apply ( isantisymmnegabgrdiffrel nataddabmonoid isplushrelnatgth ) . unfold isantisymmneg . apply isantisymmnegnatgth . Defined . Lemma isnegrelhzgth : isnegrel hzgth . Proof . apply isdecreltoisnegrel . apply isdecrelhzgth . Defined . Lemma iscoantisymmhzgth ( n m : hz ) : neg ( hzgth n m ) -> ( hzgth m n ) ⨿ ( n = m ) . Proof . revert n m. apply isantisymmnegtoiscoantisymm . apply isdecrelhzgth . intros n m . apply isantisymmneghzgth . Defined . Lemma iscotranshzgth ( n m k : hz ) : hzgth n k -> hdisj ( hzgth n m ) ( hzgth m k ) . Proof . intros gxz . destruct ( isdecrelhzgth n m ) as [ gxy | ngxy ] . apply ( hinhpr ( ii1 gxy ) ) . apply hinhpr . apply ii2 . destruct ( isdecrelhzgth m n ) as [ gyx | ngyx ] . apply ( istranshzgth _ _ _ gyx gxz ) . set ( e := isantisymmneghzgth _ _ ngxy ngyx ) . rewrite e in gxz . apply gxz . Defined . Definition istranshzlth ( n m k : hz ) : hzlth n m -> hzlth m k -> hzlth n k := λ lnm lmk, istranshzgth _ _ _ lmk lnm . Definition isirreflhzlth ( n : hz ) : neg ( hzlth n n ) := isirreflhzgth n . Lemma hzlthtoneq ( n m : hz ) ( g : hzlth n m ) : neg ( n = m ) . Proof . intros . intro e . rewrite e in g . apply ( isirreflhzlth _ g ) . Defined . Definition isasymmhzlth ( n m : hz ) : hzlth n m -> hzlth m n -> empty := λ lnm lmn, isasymmhzgth _ _ lmn lnm . Definition isantisymmneghztth ( n m : hz ) : neg ( hzlth n m ) -> neg ( hzlth m n ) -> n = m := λ nlnm nlmn, isantisymmneghzgth _ _ nlmn nlnm . Definition isnegrelhzlth : isnegrel hzlth := λ n m, isnegrelhzgth m n . Definition iscoantisymmhzlth ( n m : hz ) : neg ( hzlth n m ) -> ( hzlth m n ) ⨿ ( n = m ) . Proof . intros nlnm . destruct ( iscoantisymmhzgth m n nlnm ) as [ l | e ] . apply ( ii1 l ) . apply ( ii2 ( pathsinv0 e ) ) . Defined . Definition iscotranshzlth ( n m k : hz ) : hzlth n k -> hdisj ( hzlth n m ) ( hzlth m k ) . Proof . intros lnk . apply ( ( pr1 islogeqcommhdisj ) ( iscotranshzgth _ _ _ lnk ) ) . Defined . Definition istranshzleh ( n m k : hz ) : hzleh n m -> hzleh m k -> hzleh n k . Proof. apply istransnegrel . unfold iscotrans. apply iscotranshzgth . Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra