Library UniMath.NumberSystems.RationalNumbers

Generalities on the type of rationals and rational arithmetic. Vladimir Voevodsky . Aug. - Sep. 2011.

In this file we introduce the type hq of rationals defined as the quotient set of dirprod nat nat by the standard equivalence relation and develop the main notions of the rational arithmetic using this definition .

Preamble

Settings

Unset Kernel Term Sharing.

Imports

Require Import UniMath.Algebra.Monoids.
Require Import UniMath.Algebra.Groups.
Require Export UniMath.NumberSystems.Integers .

Opaque hz .

The commutative ring hq of integres

General definitions


Definition hq : fld := fldfrac hzintdom isdeceqhz .
Definition hqaddabgr : abgr := hq .
Definition hqmultabmonoid : abmonoid := ringmultabmonoid hq .
Definition hqtype : UU := hq .

Definition hzhztohq : hz -> ( intdomnonzerosubmonoid hzintdom ) -> hq := λ x a, setquotpr _ ( make_dirprod x a ) .

Definition hqplus : hq -> hq -> hq := @op1 hq.
Definition hqsign : hq -> hq := grinv hqaddabgr .
Definition hqminus : hq -> hq -> hq := λ x y, hqplus x ( hqsign y ) .
Definition hqzero : hq := unel hqaddabgr .

Definition hqmult : hq -> hq -> hq := @op2 hq .
Definition hqone : hq := unel hqmultabmonoid .

Declare Scope hq_scope.
Bind Scope hq_scope with hq .
Notation " x + y " := ( hqplus x y ) : hq_scope .
Notation " 0 " := hqzero : hq_scope .
Notation " 1 " := hqone : hq_scope .
Notation " - x " := ( hqsign x ) : hq_scope .
Notation " x - y " := ( hqminus x y ) : hq_scope .
Notation " x * y " := ( hqmult x y ) : hq_scope .

Delimit Scope hq_scope with hq .

Properties of equality on hq


Definition isdeceqhq : isdeceq hq := isdeceqfldfrac hzintdom isdeceqhz .

Definition isasethq := setproperty hq .

Definition hqeq ( x y : hq ) : hProp := make_hProp ( x = y ) ( isasethq _ _ ) .
Definition isdecrelhqeq : isdecrel hqeq := λ a b, isdeceqhq a b .
Definition hqdeceq : decrel hq := make_decrel isdecrelhqeq .


Definition hqbooleq := decreltobrel hqdeceq .

Definition hqneq ( x y : hq ) : hProp := make_hProp ( neg ( x = y ) ) ( isapropneg _ ) .
Definition isdecrelhqneq : isdecrel hqneq := isdecnegrel _ isdecrelhqeq .
Definition hqdecneq : decrel hq := make_decrel isdecrelhqneq .


Definition hqboolneq := decreltobrel hqdecneq .

Local Open Scope hz_scope .

Properties of addition and subtraction on hq


Local Open Scope hq_scope .

Lemma hqplusr0 ( x : hq ) : paths ( x + 0 ) x .
Show proof.
. apply ( ringrunax1 _ x ) .
.

Lemma hqplusl0 ( x : hq ) : paths ( 0 + x ) x .
Show proof.
. apply ( ringlunax1 _ x ) .
.

Lemma hqplusassoc ( x y z : hq ) : paths ( ( x + y ) + z ) ( x + ( y + z ) ) .
Show proof.
. intros . apply ( ringassoc1 hq x y z ) .
.

Lemma hqpluscomm ( x y : hq ) : paths ( x + y ) ( y + x ) .
Show proof.
. intros . apply ( ringcomm1 hq x y ) .
.

Lemma hqlminus ( x : hq ) : paths ( -x + x ) 0 .
Show proof.
. apply ( ringlinvax1 hq x ) .
.

Lemma hqrminus ( x : hq ) : paths ( x - x ) 0 .
Show proof.
. apply ( ringrinvax1 hq x ) .
.

Lemma isinclhqplusr ( n : hq ) : isincl ( λ m : hq, m + n ) .
Show proof.
apply ( pr2 ( weqtoincl ( weqrmultingr hqaddabgr n ) ) ) .

Lemma isinclhqplusl ( n : hq ) : isincl ( λ m : hq, n + m ) .
Show proof.
intro. apply ( pr2 ( weqtoincl ( weqlmultingr hqaddabgr n ) ) ) .
.

Lemma hqpluslcan ( a b c : hq ) ( is : paths ( c + a ) ( c + b ) ) : a = b .
Show proof.
. intros . apply ( @grlcan hqaddabgr a b c is ) .
.

Lemma hqplusrcan ( a b c : hq ) ( is : paths ( a + c ) ( b + c ) ) : a = b .
Show proof.
. intros . apply ( @grrcan hqaddabgr a b c is ) .
.

Definition hqinvmaponpathsminus { a b : hq } ( e : paths ( - a ) ( - b ) ) : a = b := grinvmaponpathsinv hqaddabgr e .

Properties of multiplication on hq


Lemma hqmultr1 ( x : hq ) : paths ( x * 1 ) x .
Show proof.
. apply ( ringrunax2 _ x ) .
.

Lemma hqmultl1 ( x : hq ) : paths ( 1 * x ) x .
Show proof.
. apply ( ringlunax2 _ x ) .
.

Lemma hqmult0x ( x : hq ) : paths ( 0 * x ) 0 .
Show proof.
. apply ( ringmult0x _ x ) .
.

Lemma hqmultx0 ( x : hq ) : paths ( x * 0 ) 0 .
Show proof.
. apply ( ringmultx0 _ x ) .
.

Lemma hqmultassoc ( x y z : hq ) : paths ( ( x * y ) * z ) ( x * ( y * z ) ) .
Show proof.
. intros . apply ( ringassoc2 hq x y z ) .
.

Lemma hqmultcomm ( x y : hq ) : paths ( x * y ) ( y * x ) .
Show proof.
. intros . apply ( ringcomm2 hq x y ) .
.

Multiplicative inverse and division on hq

Note : in our definition it is possible to divide by 0 . The result in this case is 0 .

Definition hqmultinv : hq -> hq := λ x, fldfracmultinv0 hzintdom isdeceqhz x .

Lemma hqislinvmultinv ( x : hq ) ( ne : hqneq x 0 ) : paths ( ( hqmultinv x ) * x ) 1 .
Show proof.
intros . apply ( islinvinfldfrac hzintdom isdeceqhz x ne ) .
.

Lemma hqisrinvmultinv ( x : hq ) ( ne : hqneq x 0 ) : paths ( x * ( hqmultinv x ) ) 1 .
Show proof.
intros . apply ( isrinvinfldfrac hzintdom isdeceqhz x ne ) .
.

Definition hqdiv ( x y : hq ) : hq := hqmult x ( hqmultinv y ) .

Definition and properties of "greater", "less", "greater or equal" and "less or equal" on hq .

Definitions and notations


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 _ ) .

Decidability


Lemma isdecrelhqgth : isdecrel hqgth .
Show proof.
. apply isdecfldfracgt . exact isasymmhzgth . apply isdecrelhzgth .
.

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 .


Properties of individual relations

hqgth

Lemma istranshqgth ( n m k : hq ) : hqgth n m -> hqgth m k -> hqgth n k .
Show proof.
apply istransfldfracgt . exact istranshzgth .
.

Lemma isirreflhqgth ( n : hq ) : neg ( hqgth n n ) .
Show proof.
apply isirreflfldfracgt . exact isirreflhzgth .
.

Lemma isasymmhqgth ( n m : hq ) : hqgth n m -> hqgth m n -> empty .
Show proof.
apply isasymmfldfracgt . exact isasymmhzgth .
.

Lemma isantisymmneghqgth ( n m : hq ) : neg ( hqgth n m ) -> neg ( hqgth m n ) -> n = m .
Show proof.
. apply isantisymmnegfldfracgt . exact isirreflhzgth . exact isantisymmneghzgth .
.

Lemma isnegrelhqgth : isnegrel hqgth .
Show proof.
. apply isdecreltoisnegrel . apply isdecrelhqgth .
.

Lemma iscoantisymmhqgth ( n m : hq ) : neg ( hqgth n m ) -> ( hqgth m n ) ⨿ ( n = m ) .
Show proof.
. revert n m. apply isantisymmnegtoiscoantisymm . apply isdecrelhqgth . intros n m . apply isantisymmneghqgth .
.

Lemma iscotranshqgth ( n m k : hq ) : hqgth n k -> hdisj ( hqgth n m ) ( hqgth m k ) .
Show 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 .
.

hqlth

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 ) .
Show proof.
. intros nlnm . destruct ( iscoantisymmhqgth m n nlnm ) as [ l | e ] . apply ( ii1 l ) . apply ( ii2 ( pathsinv0 e ) ) .
.

Definition iscotranshqlth ( n m k : hq ) : hqlth n k -> hdisj ( hqlth n m ) ( hqlth m k ) .
Show proof.
. intros lnk . apply ( ( pr1 islogeqcommhdisj ) ( iscotranshqgth _ _ _ lnk ) ) .
.

hqleh

Definition istranshqleh ( n m k : hq ) : hqleh n m -> hqleh m k -> hqleh n k .
Show proof.
apply istransnegrel . unfold iscotrans. apply iscotranshqgth .

Definition isreflhqleh ( n : hq ) : hqleh n n := isirreflhqgth n .

Definition isantisymmhqleh ( n m : hq ) : hqleh n m -> hqleh m n -> n = m := isantisymmneghqgth n m .

Definition isnegrelhqleh : isnegrel hqleh .
Show proof.
. apply isdecreltoisnegrel . apply isdecrelhqleh .
.

Definition iscoasymmhqleh ( n m : hq ) ( nl : neg ( hqleh n m ) ) : hqleh m n := negf ( isasymmhqgth _ _ ) nl .

Definition istotalhqleh : istotal hqleh .
Show proof.
. intros x y . destruct ( isdecrelhqleh x y ) as [ lxy | lyx ] . apply ( hinhpr ( ii1 lxy ) ) . apply hinhpr . apply ii2 . apply ( iscoasymmhqleh _ _ lyx ) .
.

hqgeh .

Definition istranshqgeh ( n m k : hq ) : hqgeh n m -> hqgeh m k -> hqgeh n k := λ gnm gmk, istranshqleh _ _ _ gmk gnm .

Definition isreflhqgeh ( n : hq ) : hqgeh n n := isreflhqleh _ .

Definition isantisymmhqgeh ( n m : hq ) : hqgeh n m -> hqgeh m n -> n = m := λ gnm gmn, isantisymmhqleh _ _ gmn gnm .

Definition isnegrelhqgeh : isnegrel hqgeh := λ n m, isnegrelhqleh m n .

Definition iscoasymmhqgeh ( n m : hq ) ( nl : neg ( hqgeh n m ) ) : hqgeh m n := iscoasymmhqleh _ _ nl .

Definition istotalhqgeh : istotal hqgeh := λ n m, istotalhqleh m n .

hq is archimedean


Lemma isarchhq :
  isarchfld (X := hq) hqgth.
Show proof.
  simple refine (isarchfldfrac hzintdom _ _ _ _ _ _ _ _).
  - exact isirreflhzgth.
  - exact istranshzgth.
  - apply isarchhz.

Simple implications between comparisons


Definition hqgthtogeh ( n m : hq ) : hqgth n m -> hqgeh n m .
Show proof.
intros g . apply iscoasymmhqgeh . apply ( todneg _ g ) .
.

Definition hqlthtoleh ( n m : hq ) : hqlth n m -> hqleh n m := hqgthtogeh _ _ .

Definition hqlehtoneghqgth ( n m : hq ) : hqleh n m -> neg ( hqgth n m ) .
Show proof.
intros is is' . apply ( is is' ) .
.

Definition hqgthtoneghqleh ( n m : hq ) : hqgth n m -> neg ( hqleh n m ) := λ g l , hqlehtoneghqgth _ _ l g .

Definition hqgehtoneghqlth ( n m : hq ) : hqgeh n m -> neg ( hqlth n m ) := λ gnm lnm, hqlehtoneghqgth _ _ gnm lnm .

Definition hqlthtoneghqgeh ( n m : hq ) : hqlth n m -> neg ( hqgeh n m ) := λ gnm lnm, hqlehtoneghqgth _ _ lnm gnm .

Definition neghqlehtogth ( n m : hq ) : neg ( hqleh n m ) -> hqgth n m := isnegrelhqgth n m .

Definition neghqgehtolth ( n m : hq ) : neg ( hqgeh n m ) -> hqlth n m := isnegrelhqlth n m .

Definition neghqgthtoleh ( n m : hq ) : neg ( hqgth n m ) -> hqleh n m .
Show proof.
. intros ng . destruct ( isdecrelhqleh n m ) as [ l | nl ] . apply l . destruct ( nl ng ) .
.

Definition neghqlthtogeh ( n m : hq ) : neg ( hqlth n m ) -> hqgeh n m := λ nl, neghqgthtoleh _ _ nl .

Comparison alternatives


Definition hqgthorleh ( n m : hq ) : ( hqgth n m ) ⨿ ( hqleh n m ) .
Show proof.
. intros . apply ( isdecrelhqgth n m ) .
.

Definition hqlthorgeh ( n m : hq ) : ( hqlth n m ) ⨿ ( hqgeh n m ) := hqgthorleh _ _ .

Definition hqneqchoice ( n m : hq ) ( ne : neg ( n = m ) ) : ( hqgth n m ) ⨿ ( hqlth n m ) .
Show proof.
. intros . destruct ( hqgthorleh n m ) as [ g | l ] . destruct ( hqlthorgeh n m ) as [ g' | l' ] . destruct ( isasymmhqgth _ _ g g' ) . apply ( ii1 g ) . destruct ( hqlthorgeh n m ) as [ l' | g' ] . apply ( ii2 l' ) . destruct ( ne ( isantisymmhqleh _ _ l g' ) ) .
.

Definition hqlehchoice ( n m : hq ) ( l : hqleh n m ) : ( hqlth n m ) ⨿ ( n = m ) .
Show proof.
. intros . destruct ( hqlthorgeh n m ) as [ l' | g ] . apply ( ii1 l' ) . apply ( ii2 ( isantisymmhqleh _ _ l g ) ) .
.

Definition hqgehchoice ( n m : hq ) ( g : hqgeh n m ) : ( hqgth n m ) ⨿ ( n = m ) .
Show proof.
. intros . destruct ( hqgthorleh n m ) as [ g' | l ] . apply ( ii1 g' ) . apply ( ii2 ( isantisymmhqleh _ _ l g ) ) .
.

Mixed transitivities


Lemma hqgthgehtrans ( n m k : hq ) : hqgth n m -> hqgeh m k -> hqgth n k .
Show proof.
intros gnm gmk . destruct ( hqgehchoice m k gmk ) as [ g' | e ] . apply ( istranshqgth _ _ _ gnm g' ) . rewrite e in gnm . apply gnm .

Lemma hqgehgthtrans ( n m k : hq ) : hqgeh n m -> hqgth m k -> hqgth n k .
Show proof.
intros gnm gmk . destruct ( hqgehchoice n m gnm ) as [ g' | e ] . apply ( istranshqgth _ _ _ g' gmk ) . rewrite e . apply gmk .

Lemma hqlthlehtrans ( n m k : hq ) : hqlth n m -> hqleh m k -> hqlth n k .
Show proof.
. intros l1 l2 . apply ( hqgehgthtrans k m n l2 l1 ) .
.

Lemma hqlehlthtrans ( n m k : hq ) : hqleh n m -> hqlth m k -> hqlth n k .
Show proof.
. intros l1 l2 . apply ( hqgthgehtrans k m n l2 l1 ) .
.

Addition and comparisons

gth

Definition isringaddhzgth : @isbinophrel hqaddabgr hqgth .
Show proof.
. apply isringaddfldfracgt . exact isirreflhzgth .
.

Definition hqgthandplusl ( n m k : hq ) : hqgth n m -> hqgth ( k + n ) ( k + m ) := λ g, ( pr1 isringaddhzgth ) n m k g .

Definition hqgthandplusr ( n m k : hq ) : hqgth n m -> hqgth ( n + k ) ( m + k ) := λ g, ( pr2 isringaddhzgth ) n m k g .

Definition hqgthandpluslinv ( n m k : hq ) : hqgth ( k + n ) ( k + m ) -> hqgth n m .
Show proof.
intros g . set ( g' := hqgthandplusl _ _ ( - k ) g ) . clearbody g' . rewrite ( pathsinv0 ( hqplusassoc _ _ n ) ) in g' . rewrite ( pathsinv0 ( hqplusassoc _ _ m ) ) in g' . rewrite ( hqlminus k ) in g' . rewrite ( hqplusl0 _ ) in g' . rewrite ( hqplusl0 _ ) in g' . apply g' .
.

Definition hqgthandplusrinv ( n m k : hq ) : hqgth ( n + k ) ( m + k ) -> hqgth n m .
Show proof.
intros l . rewrite ( hqpluscomm n k ) in l . rewrite ( hqpluscomm m k ) in l . apply ( hqgthandpluslinv _ _ _ l ) .
.

Lemma hqgthsnn ( n : hq ) : hqgth ( n + 1 ) n .
Show proof.
. set ( int := hqgthandplusl _ _ n ( ct ( hqgth , isdecrelhqgth , 1 , 0 ) ) ) . clearbody int . rewrite ( hqplusr0 n ) in int . apply int .
.

lth

Definition hqlthandplusl ( n m k : hq ) : hqlth n m -> hqlth ( k + n ) ( k + m ) := hqgthandplusl _ _ _ .

Definition hqlthandplusr ( n m k : hq ) : hqlth n m -> hqlth ( n + k ) ( m + k ) := hqgthandplusr _ _ _ .

Definition hqlthandpluslinv ( n m k : hq ) : hqlth ( k + n ) ( k + m ) -> hqlth n m := hqgthandpluslinv _ _ _ .

Definition hqlthandplusrinv ( n m k : hq ) : hqlth ( n + k ) ( m + k ) -> hqlth n m := hqgthandplusrinv _ _ _ .

Definition hqlthnsn ( n : hq ) : hqlth n ( n + 1 ) := hqgthsnn n .

leh

Definition hqlehandplusl ( n m k : hq ) : hqleh n m -> hqleh ( k + n ) ( k + m ) := negf ( hqgthandpluslinv n m k ) .

Definition hqlehandplusr ( n m k : hq ) : hqleh n m -> hqleh ( n + k ) ( m + k ) := negf ( hqgthandplusrinv n m k ) .

Definition hqlehandpluslinv ( n m k : hq ) : hqleh ( k + n ) ( k + m ) -> hqleh n m := negf ( hqgthandplusl n m k ) .

Definition hqlehandplusrinv ( n m k : hq ) : hqleh ( n + k ) ( m + k ) -> hqleh n m := negf ( hqgthandplusr n m k ) .

geh

Definition hqgehandplusl ( n m k : hq ) : hqgeh n m -> hqgeh ( k + n ) ( k + m ) := negf ( hqgthandpluslinv m n k ) .

Definition hqgehandplusr ( n m k : hq ) : hqgeh n m -> hqgeh ( n + k ) ( m + k ) := negf ( hqgthandplusrinv m n k ) .

Definition hqgehandpluslinv ( n m k : hq ) : hqgeh ( k + n ) ( k + m ) -> hqgeh n m := negf ( hqgthandplusl m n k ) .

Definition hqgehandplusrinv ( n m k : hq ) : hqgeh ( n + k ) ( m + k ) -> hqgeh n m := negf ( hqgthandplusr m n k ) .

Properties of hqgth in the terminology of algebra1.v


Definition isplushrelhqgth : @isbinophrel hqaddabgr hqgth := isringaddhzgth .

Lemma isinvplushrelhqgth : @isinvbinophrel hqaddabgr hqgth .
Show proof.
. split . apply hqgthandpluslinv . apply hqgthandplusrinv .
.

Lemma isringmulthqgth : isringmultgt _ hqgth .
Show proof.
. apply isringmultfldfracgt . exact isirreflhzgth .
.

Lemma isinvringmulthqgth : isinvringmultgt _ hqgth .
Show proof.
. apply isinvringmultgtif . apply isplushrelhqgth . apply isringmulthqgth . exact hqneqchoice . exact isasymmhqgth .
.

Negation and comparisons

hqgth

Lemma hqgth0andminus { n : hq } ( is : hqgth n 0 ) : hqlth ( - n ) 0 .
Show proof.
. intros . unfold hqlth . apply ( ringfromgt0 hq isplushrelhqgth is ) .
.

Lemma hqminusandgth0 { n : hq } ( is : hqgth ( - n ) 0 ) : hqlth n 0 .
Show proof.
. intros . unfold hqlth . apply ( ringtolt0 hq isplushrelhqgth is ) .
.

hqlth

Lemma hqlth0andminus { n : hq } ( is : hqlth n 0 ) : hqgth ( - n ) 0 .
Show proof.
. intros . unfold hqlth . apply ( ringfromlt0 hq isplushrelhqgth is ) .
.

Lemma hqminusandlth0 { n : hq } ( is : hqlth ( - n ) 0 ) : hqgth n 0 .
Show proof.
. intros . unfold hqlth . apply ( ringtogt0 hq isplushrelhqgth is ) .
.


hqleh

Lemma hqleh0andminus { n : hq } ( is : hqleh n 0 ) : hqgeh ( - n ) 0 .
Show proof.
. revert is. apply ( negf ( @hqminusandlth0 n ) ) .
.

Lemma hqminusandleh0 { n : hq } ( is : hqleh ( - n ) 0 ) : hqgeh n 0 .
Show proof.
. revert is. apply ( negf ( @hqlth0andminus n ) ) .
.

hqgeh

Lemma hqgeh0andminus { n : hq } ( is : hqgeh n 0 ) : hqleh ( - n ) 0 .
Show proof.
. revert is. apply ( negf ( @hqminusandgth0 n ) ) .
.

Lemma hqminusandgeh0 { n : hq } ( is : hqgeh ( - n ) 0 ) : hqleh n 0 .
Show proof.
. revert is. apply ( negf ( @hqgth0andminus n ) ) .
.

Multiplication and comparisons

gth

Definition hqgthandmultl ( n m k : hq ) ( is : hqgth k hqzero ) : hqgth n m -> hqgth ( k * n ) ( k * m ) .
Show proof.
revert n m k is. apply ( isringmultgttoislringmultgt _ isplushrelhqgth isringmulthqgth ) .
.

Definition hqgthandmultr ( n m k : hq ) ( is : hqgth k hqzero ) : hqgth n m -> hqgth ( n * k ) ( m * k ) .
Show proof.
. revert n m k is. apply ( isringmultgttoisrringmultgt _ isplushrelhqgth isringmulthqgth ) .
.

Definition hqgthandmultlinv ( n m k : hq ) ( is : hqgth k hqzero ) : hqgth ( k * n ) ( k * m ) -> hqgth n m .
Show proof.
. intros is' . apply ( isinvringmultgttoislinvringmultgt hq isplushrelhqgth isinvringmulthqgth n m k is is' ) .
.

Definition hqgthandmultrinv ( n m k : hq ) ( is : hqgth k hqzero ) : hqgth ( n * k ) ( m * k ) -> hqgth n m .
Show proof.
intros is' . apply ( isinvringmultgttoisrinvringmultgt hq isplushrelhqgth isinvringmulthqgth n m k is is' ) .
.

lth

Definition hqlthandmultl ( n m k : hq ) ( is : hqgth k 0 ) : hqlth n m -> hqlth ( k * n ) ( k * m ) := hqgthandmultl _ _ _ is .

Definition hqlthandmultr ( n m k : hq ) ( is : hqgth k 0 ) : hqlth n m -> hqlth ( n * k ) ( m * k ) := hqgthandmultr _ _ _ is .

Definition hqlthandmultlinv ( n m k : hq ) ( is : hqgth k 0 ) : hqlth ( k * n ) ( k * m ) -> hqlth n m := hqgthandmultlinv _ _ _ is .

Definition hqlthandmultrinv ( n m k : hq ) ( is : hqgth k 0 ) : hqlth ( n * k ) ( m * k ) -> hqlth n m := hqgthandmultrinv _ _ _ is .

leh

Definition hqlehandmultl ( n m k : hq ) ( is : hqgth k 0 ) : hqleh n m -> hqleh ( k * n ) ( k * m ) := negf ( hqgthandmultlinv _ _ _ is ) .

Definition hqlehandmultr ( n m k : hq ) ( is : hqgth k 0 ) : hqleh n m -> hqleh ( n * k ) ( m * k ) := negf ( hqgthandmultrinv _ _ _ is ) .

Definition hqlehandmultlinv ( n m k : hq ) ( is : hqgth k 0 ) : hqleh ( k * n ) ( k * m ) -> hqleh n m := negf ( hqgthandmultl _ _ _ is ) .

Definition hqlehandmultrinv ( n m k : hq ) ( is : hqgth k 0 ) : hqleh ( n * k ) ( m * k ) -> hqleh n m := negf ( hqgthandmultr _ _ _ is ) .

geh

Definition hqgehandmultl ( n m k : hq ) ( is : hqgth k 0 ) : hqgeh n m -> hqgeh ( k * n ) ( k * m ) := negf ( hqgthandmultlinv _ _ _ is ) .

Definition hqgehandmultr ( n m k : hq ) ( is : hqgth k 0 ) : hqgeh n m -> hqgeh ( n * k ) ( m * k ) := negf ( hqgthandmultrinv _ _ _ is ) .

Definition hqgehandmultlinv ( n m k : hq ) ( is : hqgth k 0 ) : hqgeh ( k * n ) ( k * m ) -> hqgeh n m := negf ( hqgthandmultl _ _ _ is ) .

Definition hqgehandmultrinv ( n m k : hq ) ( is : hqgth k 0 ) : hqgeh ( n * k ) ( m * k ) -> hqgeh n m := negf ( hqgthandmultr _ _ _ is ) .

Multiplication of positive with negative, negative with positive and two negatives.

Lemma hqmultgth0gth0 { m n : hq } ( ism : hqgth m 0 ) ( isn : hqgth n 0 ) : hqgth ( m * n ) 0 .
Show proof.
. intros . apply isringmulthqgth . apply ism . apply isn .
.

Lemma hqmultgth0geh0 { m n : hq } ( ism : hqgth m 0 ) ( isn : hqgeh n 0 ) : hqgeh ( m * n ) 0 .
Show proof.
. intros . destruct ( hqgehchoice _ _ isn ) as [ gn | en ] .

apply ( hqgthtogeh _ _ ( hqmultgth0gth0 ism gn ) ) .

rewrite en . rewrite ( hqmultx0 m ) . apply isreflhqgeh .
.

Lemma hqmultgeh0gth0 { m n : hq } ( ism : hqgeh m 0 ) ( isn : hqgth n 0 ) : hqgeh ( m * n ) 0 .
Show proof.
. intros . destruct ( hqgehchoice _ _ ism ) as [ gm | em ] .

apply ( hqgthtogeh _ _ ( hqmultgth0gth0 gm isn ) ) .

rewrite em . rewrite ( hqmult0x _ ) . apply isreflhqgeh .
.

Lemma hqmultgeh0geh0 { m n : hq } ( ism : hqgeh m 0 ) ( isn : hqgeh n 0 ) : hqgeh ( m * n ) 0 .
Show proof.
. intros . destruct ( hqgehchoice _ _ isn ) as [ gn | en ] .

apply ( hqmultgeh0gth0 ism gn ) .

rewrite en . rewrite ( hqmultx0 m ) . apply isreflhqgeh .
.

Lemma hqmultgth0lth0 { m n : hq } ( ism : hqgth m 0 ) ( isn : hqlth n 0 ) : hqlth ( m * n ) 0 .
Show proof.
. intros . apply ( ringmultgt0lt0 hq isplushrelhqgth isringmulthqgth ) . apply ism . apply isn .
.

Lemma hqmultgth0leh0 { m n : hq } ( ism : hqgth m 0 ) ( isn : hqleh n 0 ) : hqleh ( m * n ) 0 .
Show proof.
. intros . destruct ( hqlehchoice _ _ isn ) as [ ln | en ] .

apply ( hqlthtoleh _ _ ( hqmultgth0lth0 ism ln ) ) .

rewrite en . rewrite ( hqmultx0 m ) . apply isreflhqleh .
.

Lemma hqmultgeh0lth0 { m n : hq } ( ism : hqgeh m 0 ) ( isn : hqlth n 0 ) : hqleh ( m * n ) 0 .
Show proof.
. intros . destruct ( hqlehchoice _ _ ism ) as [ lm | em ] .

apply ( hqlthtoleh _ _ ( hqmultgth0lth0 lm isn ) ) .

destruct em . rewrite ( hqmult0x _ ) . apply isreflhqleh .
.

Lemma hqmultgeh0leh0 { m n : hq } ( ism : hqgeh m 0 ) ( isn : hqleh n 0 ) : hqleh ( m * n ) 0 .
Show proof.
. intros . destruct ( hqlehchoice _ _ isn ) as [ ln | en ] .

apply ( hqmultgeh0lth0 ism ln ) .

rewrite en . rewrite ( hqmultx0 m ) . apply isreflhqleh .
.

Lemma hqmultlth0gth0 { m n : hq } ( ism : hqlth m 0 ) ( isn : hqgth n 0 ) : hqlth ( m * n ) 0 .
Show proof.
. intros . rewrite ( hqmultcomm ) . apply hqmultgth0lth0 . apply isn . apply ism .
.

Lemma hqmultlth0geh0 { m n : hq } ( ism : hqlth m 0 ) ( isn : hqgeh n 0 ) : hqleh ( m * n ) 0 .
Show proof.
. intros . rewrite ( hqmultcomm ) . apply hqmultgeh0lth0 . apply isn . apply ism .
.

Lemma hqmultleh0gth0 { m n : hq } ( ism : hqleh m 0 ) ( isn : hqgth n 0 ) : hqleh ( m * n ) 0 .
Show proof.
. intros . rewrite ( hqmultcomm ) . apply hqmultgth0leh0 . apply isn . apply ism .
.

Lemma hqmultleh0geh0 { m n : hq } ( ism : hqleh m 0 ) ( isn : hqgeh n 0 ) : hqleh ( m * n ) 0 .
Show proof.
. intros . rewrite ( hqmultcomm ) . apply hqmultgeh0leh0 . apply isn . apply ism .
.

Lemma hqmultlth0lth0 { m n : hq } ( ism : hqlth m 0 ) ( isn : hqlth n 0 ) : hqgth ( m * n ) 0 .
Show proof.
. intros . assert ( ism' := hqlth0andminus ism ) . assert ( isn' := hqlth0andminus isn ) . assert ( int := isringmulthqgth _ _ ism' isn' ) . rewrite ( ringmultminusminus hq ) in int . apply int .
.

Lemma hqmultlth0leh0 { m n : hq } ( ism : hqlth m 0 ) ( isn : hqleh n 0 ) : hqgeh ( m * n ) 0 .
Show proof.
. intros . intros . destruct ( hqlehchoice _ _ isn ) as [ ln | en ] .

apply ( hqgthtogeh _ _ ( hqmultlth0lth0 ism ln ) ) .

rewrite en . rewrite ( hqmultx0 m ) . apply isreflhqgeh .
.

Lemma hqmultleh0lth0 { m n : hq } ( ism : hqleh m 0 ) ( isn : hqlth n 0 ) : hqgeh ( m * n ) 0 .
Show proof.
. intros . destruct ( hqlehchoice _ _ ism ) as [ lm | em ] .

apply ( hqgthtogeh _ _ ( hqmultlth0lth0 lm isn ) ) .

rewrite em . rewrite ( hqmult0x _ ) . apply isreflhqgeh .
.

Lemma hqmultleh0leh0 { m n : hq } ( ism : hqleh m 0 ) ( isn : hqleh n 0 ) : hqgeh ( m * n ) 0 .
Show proof.
. intros . destruct ( hqlehchoice _ _ isn ) as [ ln | en ] .

apply ( hqmultleh0lth0 ism ln ) .

rewrite en . rewrite ( hqmultx0 m ) . apply isreflhqgeh .
.

Cancellation properties of multiplication on hq


Lemma hqmultlcan ( a b c : hq ) ( ne : neg ( c = 0 ) ) ( e : paths ( c * a ) ( c * b ) ) : a = b .
Show proof.
. intros . apply ( intdomlcan hq _ _ _ ne e ) .
.

Lemma hqmultrcan ( a b c : hq ) ( ne : neg ( c = 0 ) ) ( e : paths ( a * c ) ( b * c ) ) : a = b .
Show proof.
. intros . apply ( intdomrcan hq _ _ _ ne e ) .
.

Positive rationals


Definition hqpos : @subabmonoid hqmultabmonoid .
Show proof.
. split with ( λ x, hqgth x 0 ) . split . intros x1 x2 . apply ( isringmulthqgth ) . apply ( pr2 x1 ) . apply ( pr2 x2 ) . apply ( ct ( hqgth , isdecrelhqgth , 1 , 0 ) ) .
.

Canonical ring homomorphism from hz to hq


Definition hztohq : hz -> hq := tofldfrac hzintdom isdeceqhz.

Definition isinclhztohq : isincl hztohq := isincltofldfrac hzintdom isdeceqhz .

Definition hztohqandneq ( n m : hz ) ( is : hzneq n m ) : hqneq ( hztohq n ) ( hztohq m ) := negf ( invmaponpathsincl _ isinclhztohq n m ) is .

Definition hztohqand0 : paths ( hztohq 0%hz ) 0 := idpath _ .

Definition hztohqand1 : paths ( hztohq 1%hz ) 1 := idpath _ .

Definition hztohqandplus ( n m : hz ) : paths ( hztohq ( n + m )%hz ) ( hztohq n + hztohq m ) := isbinop1funtofldfrac hzintdom isdeceqhz n m .

Definition hztohqandminus ( n m : hz ) : paths ( hztohq ( n - m )%hz ) ( hztohq n - hztohq m ) := tofldfracandminus hzintdom isdeceqhz n m .

Definition hztohqandmult ( n m : hz ) : paths ( hztohq ( n * m )%hz ) ( hztohq n * hztohq m ) := isbinop2funtofldfrac hzintdom isdeceqhz n m .

Definition hztohqandgth ( n m : hz ) ( is : hzgth n m ) : hqgth ( hztohq n ) ( hztohq m ) := iscomptofldfrac hzintdom isdeceqhz isplushrelhzgth isringmulthzgth ( ct ( hzgth , isdecrelhzgth , 1 , 0 )%hz ) ( hzneqchoice ) ( isasymmhzgth ) n m is .

Definition hztohqandlth ( n m : hz ) ( is : hzlth n m ) : hqlth ( hztohq n ) ( hztohq m ) := hztohqandgth m n is .

Definition hztohqandleh ( n m : hz ) ( is : hzleh n m ) : hqleh ( hztohq n ) ( hztohq m ) .
Show proof.
. intros . destruct ( hzlehchoice _ _ is ) as [ l | e ] . apply ( hqlthtoleh _ _ ( hztohqandlth _ _ l ) ) . rewrite e . apply ( isreflhqleh ) .
.

Definition hztohqandgeh ( n m : hz ) ( is : hzgeh n m ) : hqgeh ( hztohq n ) ( hztohq m ) := hztohqandleh _ _ is .

Integral part of a rational


Definition intpartint0 ( xa : dirprod hz ( intdomnonzerosubmonoid hzintdom ) ) : nat := natdiv ( hzabsval (pr1 xa ) ) ( hzabsval ( pr1 ( pr2 xa ) ) ) .

Lemma iscompintpartint0 : iscomprelfun ( eqrelabmonoidfrac hzmultabmonoid ( intdomnonzerosubmonoid hzintdom ) ) intpartint0 .
Show proof.
. Opaque hq. unfold iscomprelfun . intros xa1 xa2 . set ( x1 := pr1 xa1 ) . set ( aa1 := pr2 xa1 ) . set ( a1 := pr1 aa1 ) . set ( x2 := pr1 xa2 ) . set ( aa2 := pr2 xa2 ) . set ( a2 := pr1 aa2 ) . simpl . apply ( @hinhuniv _ ( make_hProp _ ( setproperty natset _ _ ) ) ) . intro t2 . assert ( e := pr2 t2 ) .

simpl in e . assert ( e' := ( maponpaths hzabsval ( hzmultrcan _ _ _ ( pr2 ( pr1 t2 ) ) e ) ) : paths ( hzabsval ( x1 * a2 )%hz ) ( hzabsval ( x2 * a1 )%hz ) ) . clear e . clear t2 . rewrite ( pathsinv0 ( hzabsvalandmult _ _ ) ) in e' . rewrite ( pathsinv0 ( hzabsvalandmult _ _ ) ) in e' .

unfold intpartint0 . simpl . change ( paths ( natdiv ( hzabsval x1 ) ( hzabsval a1 ) ) ( natdiv ( hzabsval x2 ) ( hzabsval a2 ) ) ) . rewrite ( pathsinv0 ( natdivandmultr (hzabsval x1 ) (hzabsval a1 ) ( hzabsval a2 ) ( hzabsvalneq0 ( pr2 aa1 ) ) ( natneq0andmult _ _ ( hzabsvalneq0 (pr2 aa1) ) ( hzabsvalneq0 (pr2 aa2) ) ) ) ) . rewrite ( pathsinv0 ( natdivandmultr (hzabsval x2 ) (hzabsval a2 ) ( hzabsval a1 ) ( hzabsvalneq0 ( pr2 aa2 ) ) ( natneq0andmult _ _ ( hzabsvalneq0 (pr2 aa2) ) ( hzabsvalneq0 (pr2 aa1) ) ) ) ) . rewrite ( natmultcomm ( hzabsval a1 ) ( hzabsval a2 ) ) . rewrite e' . apply idpath . Transparent hq .
.

Opaque iscompintpartint0 .

Definition intpart0 : hq -> nat := setquotuniv ( eqrelabmonoidfrac hzmultabmonoid (intdomnonzerosubmonoid hzintdom) ) natset _
     ( iscompintpartint0 ) .

Definition intpart ( x : hq ) : hz .
Show proof.
. destruct ( hqlthorgeh x 0 ) as [ l | ge ] . destruct ( isdeceqhq ( x + ( hztohq ( nattohz ( intpart0 x ) ) ) ) 0 ) as [ e | ne ] .

apply ( - (nattohz (intpart0 x)))%hz .

apply ( - ( 1 + (nattohz (intpart0 x)) ) )%hz .

apply (nattohz (intpart0 x)) .
.