proposition: Lemma isinclhqplusl ( n : hq ) : isincl ( λ m : hq, n + m ) .
proof: Proof. intro. apply ( pr2 ( weqtoincl ( weqlmultingr hqaddabgr n ) ) ) . Defined . Lemma hqpluslcan ( a b c : hq ) ( is : paths ( c + a ) ( c + b ) ) : a = b . Proof . intros . apply ( @grlcan hqaddabgr a b c is ) . Defined . Lemma hqplusrcan ( a b c : hq ) ( is : paths ( a + c ) ( b + c ) ) : a = b . Proof . intros . apply ( @grrcan hqaddabgr a b c is ) . Defined . Definition hqinvmaponpathsminus { a b : hq } ( e : paths ( - a ) ( - b ) ) : a = b := grinvmaponpathsinv hqaddabgr e . Lemma hqmultr1 ( x : hq ) : paths ( x * 1 ) x . Proof . apply ( ringrunax2 _ x ) . Defined . Lemma hqmultl1 ( x : hq ) : paths ( 1 * x ) x . Proof . apply ( ringlunax2 _ x ) . Defined . Lemma hqmult0x ( x : hq ) : paths ( 0 * x ) 0 . Proof . apply ( ringmult0x _ x ) . Defined . Lemma hqmultx0 ( x : hq ) : paths ( x * 0 ) 0 . Proof . apply ( ringmultx0 _ x ) . Defined . Lemma hqmultassoc ( x y z : hq ) : paths ( ( x * y ) * z ) ( x * ( y * z ) ) . Proof . intros . apply ( ringassoc2 hq x y z ) . Defined . Lemma hqmultcomm ( x y : hq ) : paths ( x * y ) ( y * x ) . Proof . intros . apply ( ringcomm2 hq x y ) . Defined . Definition hqmultinv : hq -> hq := λ x, fldfracmultinv0 hzintdom isdeceqhz x . Lemma hqislinvmultinv ( x : hq ) ( ne : hqneq x 0 ) : paths ( ( hqmultinv x ) * x ) 1 . Proof. intros . apply ( islinvinfldfrac hzintdom isdeceqhz x ne ) . Defined . Lemma hqisrinvmultinv ( x : hq ) ( ne : hqneq x 0 ) : paths ( x * ( hqmultinv x ) ) 1 . Proof. intros . apply ( isrinvinfldfrac hzintdom isdeceqhz x ne ) . Defined . Definition hqdiv ( x y : hq ) : hq := hqmult x ( hqmultinv y ) . Definition hqgth : hrel hq := fldfracgt hzintdom isdeceqhz isplushrelhzgth isringmulthzgth ( ct ( hzgth , isdecrelhzgth, 1%hz , 0%hz ) ) hzneqchoice . Definition hqlth : hrel hq := λ a b, hqgth b a . Definition hqleh : hrel hq := λ a b, make_hProp ( neg ( hqgth a b ) ) ( isapropneg _ ) . Definition hqgeh : hrel hq := λ a b, make_hProp ( neg ( hqgth b a ) ) ( isapropneg _ ) . Lemma isdecrelhqgth : isdecrel hqgth . Proof . apply isdecfldfracgt . exact isasymmhzgth . apply isdecrelhzgth . Defined . Definition hqgthdec := make_decrel isdecrelhqgth . Definition isdecrelhqlth : isdecrel hqlth := λ x x', isdecrelhqgth x' x . Definition hqlthdec := make_decrel isdecrelhqlth . Definition isdecrelhqleh : isdecrel hqleh := isdecnegrel _ isdecrelhqgth . Definition hqlehdec := make_decrel isdecrelhqleh . Definition isdecrelhqgeh : isdecrel hqgeh := λ x x', isdecrelhqleh x' x . Definition hqgehdec := make_decrel isdecrelhqgeh . Lemma istranshqgth ( n m k : hq ) : hqgth n m -> hqgth m k -> hqgth n k . Proof. apply istransfldfracgt . exact istranshzgth . Defined . Lemma isirreflhqgth ( n : hq ) : neg ( hqgth n n ) . Proof. apply isirreflfldfracgt . exact isirreflhzgth . Defined . Lemma isasymmhqgth ( n m : hq ) : hqgth n m -> hqgth m n -> empty . Proof. apply isasymmfldfracgt . exact isasymmhzgth . Defined . Lemma isantisymmneghqgth ( n m : hq ) : neg ( hqgth n m ) -> neg ( hqgth m n ) -> n = m . Proof . apply isantisymmnegfldfracgt . exact isirreflhzgth . exact isantisymmneghzgth . Defined . Lemma isnegrelhqgth : isnegrel hqgth . Proof . apply isdecreltoisnegrel . apply isdecrelhqgth . Defined . Lemma iscoantisymmhqgth ( n m : hq ) : neg ( hqgth n m ) -> ( hqgth m n ) ⨿ ( n = m ) . Proof . revert n m. apply isantisymmnegtoiscoantisymm . apply isdecrelhqgth . intros n m . apply isantisymmneghqgth . Defined . Lemma iscotranshqgth ( n m k : hq ) : hqgth n k -> hdisj ( hqgth n m ) ( hqgth m k ) . Proof . intros gnk . destruct ( isdecrelhqgth n m ) as [ gxy | ngxy ] . apply ( hinhpr ( ii1 gxy ) ) . apply hinhpr . apply ii2 . destruct ( isdecrelhqgth m n ) as [ gyx | ngyx ] . apply ( istranshqgth _ _ _ gyx gnk ) . set ( e := isantisymmneghqgth _ _ ngxy ngyx ) . rewrite e in gnk . apply gnk . Defined . Definition istranshqlth ( n m k : hq ) : hqlth n m -> hqlth m k -> hqlth n k := λ lnm lmk, istranshqgth _ _ _ lmk lnm . Definition isirreflhqlth ( n : hq ) : neg ( hqlth n n ) := isirreflhqgth n . Definition isasymmhqlth ( n m : hq ) : hqlth n m -> hqlth m n -> empty := λ lnm lmn, isasymmhqgth _ _ lmn lnm . Definition isantisymmneghqtth ( n m : hq ) : neg ( hqlth n m ) -> neg ( hqlth m n ) -> n = m := λ nlnm nlmn, isantisymmneghqgth _ _ nlmn nlnm . Definition isnegrelhqlth : isnegrel hqlth := λ n m, isnegrelhqgth m n . Definition iscoantisymmhqlth ( n m : hq ) : neg ( hqlth n m ) -> ( hqlth m n ) ⨿ ( n = m ) . Proof . intros nlnm . destruct ( iscoantisymmhqgth m n nlnm ) as [ l | e ] . apply ( ii1 l ) . apply ( ii2 ( pathsinv0 e ) ) . Defined . Definition iscotranshqlth ( n m k : hq ) : hqlth n k -> hdisj ( hqlth n m ) ( hqlth m k ) . Proof . intros lnk . apply ( ( pr1 islogeqcommhdisj ) ( iscotranshqgth _ _ _ lnk ) ) . Defined . Definition istranshqleh ( n m k : hq ) : hqleh n m -> hqleh m k -> hqleh n k . Proof. apply istransnegrel . unfold iscotrans. apply iscotranshqgth . Defined.
imports: UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.NumberSystems.Integers 