Library hnat
Natural numbers and their properties. Vladimir Voevodsky . Apr. - Sep. 2011
Preamble
Unset Automatic Introduction.
Imports.
Require Export Foundations.hlevel2.algebra1d .
To up-stream files
Equality on nat
Basic properties of paths on nat and the proofs of isdeceq and isaset for nat .
Lemma negpaths0sx ( x : nat ) : neg ( paths O (S x) ) .
Proof. intro. set (f:= fun n : nat => match n with O => true | S m => false end ) . apply ( negf ( @maponpaths _ _ f 0 ( S x ) ) nopathstruetofalse ) . Defined.
Lemma negpathssx0 ( x : nat ) : neg ( paths (S x) O ) .
Proof. intros x X. apply (negpaths0sx x (pathsinv0 X)). Defined.
Lemma invmaponpathsS ( n m : nat ) : paths ( S n ) ( S m ) -> paths n m .
Proof. intros n m e . set ( f := fun n : nat => match n with O => O | S m => m end ) . apply ( @maponpaths _ _ f ( S n ) ( S m ) e ) . Defined.
Lemma noeqinjS ( x x' : nat ) : neg ( paths x x' ) -> neg ( paths (S x) (S x') ) .
Proof. intros x x'. apply ( negf ( invmaponpathsS x x' ) ) . Defined.
Definition isdeceqnat: isdeceq nat.
Proof. unfold isdeceq. intro x . induction x as [ | x IHx ] . intro x' . destruct x'. apply ( ii1 ( idpath O ) ) . apply ( ii2 ( negpaths0sx x' ) ) . intro x' . destruct x'. apply ( ii2 (negpathssx0 x ) ) . destruct ( IHx x' ) as [ p | e ]. apply ( ii1 ( maponpaths S p ) ) . apply ( ii2 ( noeqinjS _ _ e ) ) . Defined .
Definition isisolatedn ( n : nat ) : isisolated _ n .
Proof. intro. unfold isisolated . intro x' . apply isdeceqnat . Defined.
Theorem isasetnat: isaset nat.
Proof. apply (isasetifdeceq _ isdeceqnat). Defined.
Definition natset : hSet := hSetpair _ isasetnat .
Definition nateq ( x y : nat ) : hProp := hProppair ( paths x y ) ( isasetnat _ _ ) .
Definition isdecrelnateq : isdecrel nateq := fun a b => isdeceqnat a b .
Definition natdeceq : decrel nat := decrelpair isdecrelnateq .
Definition natbooleq := decreltobrel natdeceq .
Definition natneq ( x y : nat ) : hProp := hProppair ( neg ( paths x y ) ) ( isapropneg _ ) .
Definition isdecrelnatneq : isdecrel natneq := isdecnegrel _ isdecrelnateq .
Definition natdecneq : decrel nat := decrelpair isdecrelnatneq .
Definition natboolneq := decreltobrel natdecneq .
Theorem isinclS : isincl S .
Proof. apply ( isinclbetweensets S isasetnat isasetnat invmaponpathsS ) . Defined .
Theorem isdecinclS : isdecincl S .
Proof. intro n . apply isdecpropif . apply ( isinclS n ) . destruct n as [ | n ] . assert ( nh : neg ( hfiber S 0 ) ) . intro hf . destruct hf as [ m e ] . apply ( negpathssx0 _ e ) . apply ( ii2 nh ) . apply ( ii1 ( hfiberpair _ n ( idpath _ ) ) ) . Defined .
Fixpoint natgtb (n m : nat) : bool :=
match n , m with
| S n , S m => natgtb n m
| O, _ => false
| _, _ => true
end.
Semi-boolean "greater" on nat or natgth
Definition natgth ( n m : nat ) := hProppair ( paths ( natgtb n m ) true ) ( isasetbool _ _ ) .
Notation " x > y " := ( natgth x y ) : nat_scope .
Lemma negnatgth0n ( n : nat ) : neg ( natgth 0 n ) .
Proof. intro n . simpl . intro np . apply ( nopathsfalsetotrue np ) . Defined .
Lemma natgthsnn ( n : nat ) : natgth ( S n ) n .
Proof . intro . induction n as [ | n IHn ] . simpl . apply idpath . apply IHn . Defined .
Lemma natgthsn0 ( n : nat ) : natgth ( S n ) 0 .
Proof . intro . simpl . apply idpath . Defined .
Lemma negnatgth0tois0 ( n : nat ) ( ng : neg ( natgth n 0 ) ) : paths n 0 .
Proof . intro. destruct n as [ | n ] . intro. apply idpath. intro ng . destruct ( ng ( natgthsn0 _ ) ) . Defined .
Lemma natneq0togth0 ( n : nat ) ( ne : neg ( paths n 0 ) ) : natgth n 0 .
Proof . intros . destruct n as [ | n ] . destruct ( ne ( idpath _ ) ) . apply natgthsn0 . Defined .
Lemma nat1gthtois0 ( n : nat ) ( g : natgth 1 n ) : paths n 0 .
Proof . intro . destruct n as [ | n ] . intro . apply idpath . intro x . destruct ( negnatgth0n n x ) . Defined .
Lemma istransnatgth ( n m k : nat ) : natgth n m -> natgth m k -> natgth n k .
Proof. intro. induction n as [ | n IHn ] . intros m k g . destruct ( negnatgth0n _ g ) . intro m . destruct m as [ | m ] . intros k g g' . destruct ( negnatgth0n _ g' ) . intro k . destruct k as [ | k ] . intros . apply natgthsn0 . apply ( IHn m k ) . Defined.
Lemma isirreflnatgth ( n : nat ) : neg ( natgth n n ) .
Proof. intro . induction n as [ | n IHn ] . apply ( negnatgth0n 0 ) . apply IHn . Defined .
Notation negnatlthnn := isirreflnatgth .
Lemma natgthtoneq ( n m : nat ) ( g : natgth n m ) : neg ( paths n m ) .
Proof . intros . intro e . rewrite e in g . apply ( isirreflnatgth _ g ) . Defined .
Lemma isasymmnatgth ( n m : nat ) : natgth n m -> natgth m n -> empty .
Proof. intros n m is is' . apply ( isirreflnatgth n ( istransnatgth _ _ _ is is' ) ) . Defined .
Lemma isantisymmnegnatgth ( n m : nat ) : neg ( natgth n m ) -> neg ( natgth m n ) -> paths n m .
Proof . intro n . induction n as [ | n IHn ] . intros m ng0m ngm0 . apply ( pathsinv0 ( negnatgth0tois0 _ ngm0 ) ) . intro m . destruct m as [ | m ] . intros ngsn0 ng0sn . destruct ( ngsn0 ( natgthsn0 _ ) ) . intros ng1 ng2 . apply ( maponpaths S ( IHn m ng1 ng2 ) ) . Defined .
Lemma isdecrelnatgth : isdecrel natgth .
Proof. intros n m . apply ( isdeceqbool ( natgtb n m ) true ) . Defined .
Definition natgthdec := decrelpair isdecrelnatgth .
Lemma isnegrelnatgth : isnegrel natgth .
Proof . apply isdecreltoisnegrel . apply isdecrelnatgth . Defined .
Lemma iscoantisymmnatgth ( n m : nat ) : neg ( natgth n m ) -> coprod ( natgth m n ) ( paths n m ) .
Proof . apply isantisymmnegtoiscoantisymm . apply isdecrelnatgth . intros n m . apply isantisymmnegnatgth . Defined .
Lemma iscotransnatgth ( n m k : nat ) : natgth n k -> hdisj ( natgth n m ) ( natgth m k ) .
Proof . intros x y z gxz . destruct ( isdecrelnatgth x y ) as [ gxy | ngxy ] . apply ( hinhpr _ ( ii1 gxy ) ) . apply hinhpr . apply ii2 . destruct ( isdecrelnatgth y x ) as [ gyx | ngyx ] . apply ( istransnatgth _ _ _ gyx gxz ) . set ( e := isantisymmnegnatgth _ _ ngxy ngyx ) . rewrite e in gxz . apply gxz . Defined .
Definition natlth ( n m : nat ) := natgth m n .
Notation " x < y " := ( natlth x y ) : nat_scope .
Definition negnatlthn0 ( n : nat ) : neg ( natlth n 0 ) := negnatgth0n n .
Definition natlthnsn ( n : nat ) : natlth n ( S n ) := natgthsnn n .
Definition negnat0lthtois0 ( n : nat ) ( nl : neg ( natlth 0 n ) ) : paths n 0 := negnatgth0tois0 n nl .
Definition natneq0to0lth ( n : nat ) ( ne : neg ( paths n 0 ) ) : natlth 0 n := natneq0togth0 n ne .
Definition natlth1tois0 ( n : nat ) ( l : natlth n 1 ) : paths n 0 := nat1gthtois0 _ l .
Definition istransnatlth ( n m k : nat ) : natlth n m -> natlth m k -> natlth n k := fun lnm lmk => istransnatgth _ _ _ lmk lnm .
Definition isirreflnatlth ( n : nat ) : neg ( natlth n n ) := isirreflnatgth n .
Notation negnatgthnn := isirreflnatlth .
Lemma natlthtoneq ( n m : nat ) ( g : natlth n m ) : neg ( paths n m ) .
Proof . intros . intro e . rewrite e in g . apply ( isirreflnatlth _ g ) . Defined .
Definition isasymmnatlth ( n m : nat ) : natlth n m -> natlth m n -> empty := fun lnm lmn => isasymmnatgth _ _ lmn lnm .
Definition isantisymmnegnattth ( n m : nat ) : neg ( natlth n m ) -> neg ( natlth m n ) -> paths n m := fun nlnm nlmn => isantisymmnegnatgth _ _ nlmn nlnm .
Definition isdecrelnatlth : isdecrel natlth := fun n m => isdecrelnatgth m n .
Definition natlthdec := decrelpair isdecrelnatlth .
Definition isnegrelnatlth : isnegrel natlth := fun n m => isnegrelnatgth m n .
Definition iscoantisymmnatlth ( n m : nat ) : neg ( natlth n m ) -> coprod ( natlth m n ) ( paths n m ) .
Proof . intros n m nlnm . destruct ( iscoantisymmnatgth m n nlnm ) as [ l | e ] . apply ( ii1 l ) . apply ( ii2 ( pathsinv0 e ) ) . Defined .
Definition iscotransnatlth ( n m k : nat ) : natlth n k -> hdisj ( natlth n m ) ( natlth m k ) .
Proof . intros n m k lnk . apply ( ( pr1 islogeqcommhdisj ) ( iscotransnatgth _ _ _ lnk ) ) . Defined .
Definition natleh ( n m : nat ) := hProppair ( neg ( natgth n m ) ) ( isapropneg _ ) .
Notation " x <= y " := ( natleh x y ) : nat_scope .
Definition natleh0tois0 ( n : nat ) ( l : natleh n 0 ) : paths n 0 := negnatgth0tois0 _ l .
Definition natleh0n ( n : nat ) : natleh 0 n := negnatgth0n _ .
Definition negnatlehsn0 ( n : nat ) : neg ( natleh ( S n ) 0 ) := todneg _ ( natgthsn0 n ) .
Definition negnatlehsnn ( n : nat ) : neg ( natleh ( S n ) n ) := todneg _ ( natgthsnn _ ) .
Definition istransnatleh ( n m k : nat ) : natleh n m -> natleh m k -> natleh n k .
Proof. apply istransnegrel . unfold iscotrans. apply iscotransnatgth . Defined.
Definition isreflnatleh ( n : nat ) : natleh n n := isirreflnatgth n .
Definition isantisymmnatleh ( n m : nat ) : natleh n m -> natleh m n -> paths n m := isantisymmnegnatgth n m .
Definition isdecrelnatleh : isdecrel natleh := isdecnegrel _ isdecrelnatgth .
Definition natlehdec := decrelpair isdecrelnatleh .
Definition isnegrelnatleh : isnegrel natleh .
Proof . apply isdecreltoisnegrel . apply isdecrelnatleh . Defined .
Definition iscoasymmnatleh ( n m : nat ) ( nl : neg ( natleh n m ) ) : natleh m n := negf ( isasymmnatgth _ _ ) nl .
Definition istotalnatleh : istotal natleh .
Proof . intros x y . destruct ( isdecrelnatleh x y ) as [ lxy | lyx ] . apply ( hinhpr _ ( ii1 lxy ) ) . apply hinhpr . apply ii2 . apply ( iscoasymmnatleh _ _ lyx ) . Defined .
Definition natgeh ( n m : nat ) : hProp := hProppair ( neg ( natgth m n ) ) ( isapropneg _ ) .
Notation " x >= y " := ( natgeh x y ) : nat_scope .
Definition nat0gehtois0 ( n : nat ) ( g : natgeh 0 n ) : paths n 0 := natleh0tois0 _ g .
Definition natgehn0 ( n : nat ) : natgeh n 0 := natleh0n n .
Definition negnatgeh0sn ( n : nat ) : neg ( natgeh 0 ( S n ) ) := negnatlehsn0 n .
Definition negnatgehnsn ( n : nat ) : neg ( natgeh n ( S n ) ) := negnatlehsnn n .
Definition istransnatgeh ( n m k : nat ) : natgeh n m -> natgeh m k -> natgeh n k := fun gnm gmk => istransnatleh _ _ _ gmk gnm .
Definition isreflnatgeh ( n : nat ) : natgeh n n := isreflnatleh _ .
Definition isantisymmnatgeh ( n m : nat ) : natgeh n m -> natgeh m n -> paths n m := fun gnm gmn => isantisymmnatleh _ _ gmn gnm .
Definition isdecrelnatgeh : isdecrel natgeh := fun n m => isdecrelnatleh m n .
Definition natgehdec := decrelpair isdecrelnatgeh .
Definition isnegrelnatgeh : isnegrel natgeh := fun n m => isnegrelnatleh m n .
Definition iscoasymmnatgeh ( n m : nat ) ( nl : neg ( natgeh n m ) ) : natgeh m n := iscoasymmnatleh _ _ nl .
Definition istotalnatgeh : istotal natgeh := fun n m => istotalnatleh m n .
Definition natgthtogeh ( n m : nat ) : natgth n m -> natgeh n m .
Proof. intros n m g . apply iscoasymmnatgeh . apply ( todneg _ g ) . Defined .
Definition natlthtoleh ( n m : nat ) : natlth n m -> natleh n m := natgthtogeh _ _ .
Definition natlehtonegnatgth ( n m : nat ) : natleh n m -> neg ( natgth n m ) .
Proof. intros n m is is' . apply ( is is' ) . Defined .
Definition natgthtonegnatleh ( n m : nat ) : natgth n m -> neg ( natleh n m ) := fun g l => natlehtonegnatgth _ _ l g .
Definition natgehtonegnatlth ( n m : nat ) : natgeh n m -> neg ( natlth n m ) := fun gnm lnm => natlehtonegnatgth _ _ gnm lnm .
Definition natlthtonegnatgeh ( n m : nat ) : natlth n m -> neg ( natgeh n m ) := fun gnm lnm => natlehtonegnatgth _ _ lnm gnm .
Definition negnatlehtogth ( n m : nat ) : neg ( natleh n m ) -> natgth n m := isnegrelnatgth n m .
Definition negnatgehtolth ( n m : nat ) : neg ( natgeh n m ) -> natlth n m := isnegrelnatlth n m .
Definition negnatgthtoleh ( n m : nat ) : neg ( natgth n m ) -> natleh n m .
Proof . intros n m ng . destruct ( isdecrelnatleh n m ) as [ l | nl ] . apply l . destruct ( nl ng ) . Defined .
Definition negnatlthtogeh ( n m : nat ) : neg ( natlth n m ) -> natgeh n m := fun nl => negnatgthtoleh _ _ nl .
Definition natlehnsn ( n : nat ) : natleh n ( S n ) := natlthtoleh _ _ ( natgthsnn n ) .
Definition natgehsnn ( n : nat ) : natgeh ( S n ) n := natlehnsn n .
Definition natgthorleh ( n m : nat ) : coprod ( natgth n m ) ( natleh n m ) .
Proof . intros . apply ( isdecrelnatgth n m ) . Defined .
Definition natlthorgeh ( n m : nat ) : coprod ( natlth n m ) ( natgeh n m ) := natgthorleh _ _ .
Definition natneqchoice ( n m : nat ) ( ne : neg ( paths n m ) ) : coprod ( natgth n m ) ( natlth n m ) .
Proof . intros . destruct ( natgthorleh n m ) as [ l | g ] . apply ( ii1 l ) . destruct ( natlthorgeh n m ) as [ l' | g' ] . apply ( ii2 l' ) . destruct ( ne ( isantisymmnatleh _ _ g g' ) ) . Defined .
Definition natlehchoice ( n m : nat ) ( l : natleh n m ) : coprod ( natlth n m ) ( paths n m ) .
Proof . intros . destruct ( natlthorgeh n m ) as [ l' | g ] . apply ( ii1 l' ) . apply ( ii2 ( isantisymmnatleh _ _ l g ) ) . Defined .
Definition natgehchoice ( n m : nat ) ( g : natgeh n m ) : coprod ( natgth n m ) ( paths n m ) .
Proof . intros . destruct ( natgthorleh n m ) as [ g' | l ] . apply ( ii1 g' ) . apply ( ii2 ( isantisymmnatleh _ _ l g ) ) . Defined .
Lemma natgthgehtrans ( n m k : nat ) : natgth n m -> natgeh m k -> natgth n k .
Proof. intros n m k gnm gmk . destruct ( natgehchoice m k gmk ) as [ g' | e ] . apply ( istransnatgth _ _ _ gnm g' ) . rewrite e in gnm . apply gnm . Defined.
Lemma natgehgthtrans ( n m k : nat ) : natgeh n m -> natgth m k -> natgth n k .
Proof. intros n m k gnm gmk . destruct ( natgehchoice n m gnm ) as [ g' | e ] . apply ( istransnatgth _ _ _ g' gmk ) . rewrite e . apply gmk . Defined.
Lemma natlthlehtrans ( n m k : nat ) : natlth n m -> natleh m k -> natlth n k .
Proof . intros n m k l1 l2 . apply ( natgehgthtrans k m n l2 l1 ) . Defined .
Lemma natlehlthtrans ( n m k : nat ) : natleh n m -> natlth m k -> natlth n k .
Proof . intros n m k l1 l2 . apply ( natgthgehtrans k m n l2 l1 ) . Defined .
Lemma natgthtogehsn ( n m : nat ) : natgth n m -> natgeh n ( S m ) .
Proof. intro n . induction n as [ | n IHn ] . intros m X . destruct ( negnatgth0n _ X ) . intros m X . destruct m as [ | m ] . apply ( natgehn0 n ) . apply ( IHn m X ) . Defined .
Lemma natgthsntogeh ( n m : nat ) : natgth ( S n ) m -> natgeh n m .
Proof. intros n m a . apply ( natgthtogehsn ( S n ) m a ) . Defined.
Lemma natgehtogthsn ( n m : nat ) : natgeh n m -> natgth ( S n ) m .
Proof . intros n m X . apply ( natgthgehtrans _ n _ ) . apply natgthsnn . apply X . Defined.
Lemma natgehsntogth ( n m : nat ) : natgeh n ( S m ) -> natgth n m .
Proof. intros n m X . apply ( natgehgthtrans _ ( S m ) _ X ) . apply natgthsnn . Defined .
Lemma natlthtolehsn ( n m : nat ) : natlth n m -> natleh ( S n ) m .
Proof. intros n m X . apply ( natgthtogehsn m n X ) . Defined .
Lemma natlehsntolth ( n m : nat ) : natleh ( S n ) m -> natlth n m .
Proof. intros n m X . apply ( natgehsntogth m n X ) . Defined .
Lemma natlehtolthsn ( n m : nat ) : natleh n m -> natlth n ( S m ) .
Proof. intros n m X . apply ( natgehtogthsn m n X ) . Defined.
Lemma natlthsntoleh ( n m : nat ) : natlth n ( S m ) -> natleh n m .
Proof. intros n m a . apply ( natlthtolehsn n ( S m ) a ) . Defined.
Lemma natlehchoice2 ( n m : nat ) : natleh n m -> coprod ( natleh ( S n ) m ) ( paths n m ) .
Proof . intros n m l . destruct ( natlehchoice n m l ) as [ l' | e ] . apply ( ii1 ( natlthtolehsn _ _ l' ) ) . apply ( ii2 e ) . Defined .
Lemma natgehchoice2 ( n m : nat ) : natgeh n m -> coprod ( natgeh n ( S m ) ) ( paths n m ) .
Proof . intros n m g . destruct ( natgehchoice n m g ) as [ g' | e ] . apply ( ii1 ( natgthtogehsn _ _ g' ) ) . apply ( ii2 e ) . Defined .
Lemma natgthchoice2 ( n m : nat ) : natgth n m -> coprod ( natgth n ( S m ) ) ( paths n ( S m ) ) .
Proof. intros n m g . destruct ( natgehchoice _ _ ( natgthtogehsn _ _ g ) ) as [ g' | e ] . apply ( ii1 g' ) . apply ( ii2 e ) . Defined .
Lemma natlthchoice2 ( n m : nat ) : natlth n m -> coprod ( natlth ( S n ) m ) ( paths ( S n ) m ) .
Proof. intros n m l . destruct ( natlehchoice _ _ ( natlthtolehsn _ _ l ) ) as [ l' | e ] . apply ( ii1 l' ) . apply ( ii2 e ) . Defined .
Lemma natplusl0 ( n : nat ) : 0 + n = n .
Proof . intros . apply idpath . Defined .
Lemma natplusr0 ( n : nat ) : n + 0 = n .
Proof .
intro . induction n as [ | n IH n ] . apply idpath . simpl . apply ( maponpaths S IH ) .
Defined .
Hint Resolve natplusr0: natarith .
Lemma natplusnsm ( n m : nat ) : n + S m = S n + m .
Proof. intro . simpl . induction n as [ | n IHn ] . auto with natarith . simpl . intro . apply ( maponpaths S ( IHn m ) ) . Defined .
Hint Resolve natplusnsm : natarith .
Lemma natpluscomm ( n m : nat ) : n + m = m + n .
Proof. intro. induction n as [ | n IHn ] . intro . auto with natarith . intro . set ( int := IHn ( S m ) ) . set ( int2 := pathsinv0 ( natplusnsm n m ) ) . set ( int3 := pathsinv0 ( natplusnsm m n ) ) . set ( int4 := pathscomp0 int2 int ) . apply ( pathscomp0 int4 int3 ) . Defined .
Hint Resolve natpluscomm : natarith .
Lemma natplusassoc ( n m k : nat ) : paths ( ( n + m ) + k ) ( n + ( m + k ) ) .
Proof . intro . induction n as [ | n IHn ] . auto with natarith . intros . simpl . apply ( maponpaths S ( IHn m k ) ) . Defined.
Hint Resolve natplusassoc : natarith .
Definition nataddabmonoid : abmonoid := abmonoidpair ( setwithbinoppair natset ( fun n m : nat => n + m ) ) ( dirprodpair ( dirprodpair natplusassoc ( @isunitalpair natset _ 0 ( dirprodpair natplusl0 natplusr0 ) ) ) natpluscomm ) .
Definition natgthtogths ( n m : nat ) : natgth n m -> natgth ( S n ) m .
Proof. intros n m is . apply ( istransnatgth _ _ _ ( natgthsnn n ) is ) . Defined .
Definition negnatgthmplusnm ( n m : nat ) : neg ( natgth m ( n + m ) ) .
Proof. intros . induction n as [ | n IHn ] . apply isirreflnatgth .
apply ( istransnatleh _ _ _ IHn ( ( natlthtoleh _ _ ( natlthnsn _ ) ) ) ) . Defined .
Definition negnatgthnplusnm ( n m : nat ) : neg ( natgth n ( n + m ) ) .
Proof. intros . rewrite ( natpluscomm n m ) . apply ( negnatgthmplusnm m n ) . Defined .
Definition natgthandplusl ( n m k : nat ) : natgth n m -> natgth ( k + n ) ( k + m ) .
Proof. intros n m k l . induction k as [ | k IHk ] . assumption . assumption . Defined .
Definition natgthandplusr ( n m k : nat ) : natgth n m -> natgth ( n + k ) ( m + k ) .
Proof. intros . rewrite ( natpluscomm n k ) . rewrite ( natpluscomm m k ) .
apply natgthandplusl . assumption . Defined .
Definition natgthandpluslinv ( n m k : nat ) : natgth ( k + n ) ( k + m ) -> natgth n m .
Proof.
intros n m k l . induction k as [ | k IHk ] . assumption . apply ( IHk l ) .
Defined .
Definition natgthandplusrinv ( n m k : nat ) : natgth ( n + k ) ( m + k ) -> natgth n m .
Proof. intros n m k l . rewrite ( natpluscomm n k ) in l . rewrite ( natpluscomm m k ) in l .
apply ( natgthandpluslinv _ _ _ l ) .
Defined .
natlth
Definition natlthtolths ( n m : nat ) : natlth n m -> natlth n ( S m ) := natgthtogths _ _ .
Definition negnatlthplusnmm ( n m : nat ) : neg ( natlth ( n + m ) m ) := negnatgthmplusnm _ _ .
Definition negnatlthplusnmn ( n m : nat ) : neg ( natlth ( n + m ) n ) := negnatgthnplusnm _ _ .
Definition natlthandplusl ( n m k : nat ) : natlth n m -> natlth ( k + n ) ( k + m ) := natgthandplusl _ _ _ .
Definition natlthandplusr ( n m k : nat ) : natlth n m -> natlth ( n + k ) ( m + k ) := natgthandplusr _ _ _ .
Definition natlthandpluslinv ( n m k : nat ) : natlth ( k + n ) ( k + m ) -> natlth n m := natgthandpluslinv _ _ _ .
Definition natlthandplusrinv ( n m k : nat ) : natlth ( n + k ) ( m + k ) -> natlth n m := natgthandplusrinv _ _ _ .
natleh
Definition natlehtolehs ( n m : nat ) : n <= m -> n <= S m .
Proof .
intros n m is . apply ( istransnatleh _ _ _ is ( natlthtoleh _ _ ( natlthnsn _ ) ) ) .
Defined .
Definition natlehmplusnm ( n m : nat ) : m <= n + m :=
negnatlthplusnmm _ _ .
Definition natlehnplusnm ( n m : nat ) : n <= n + m :=
negnatlthplusnmn _ _ .
Definition natlehandplusl ( n m k : nat ) : n <= m -> k + n <= k + m :=
negf ( natgthandpluslinv n m k ) .
Definition natlehandplusr ( n m k : nat ) : n <= m -> n + k <= m + k :=
negf ( natgthandplusrinv n m k ) .
Definition natlehandpluslinv ( n m k : nat ) : k + n <= k + m -> n <= m :=
negf ( natgthandplusl n m k ) .
Definition natlehandplusrinv ( n m k : nat ) : n + k <= m + k -> n <= m :=
negf ( natgthandplusr n m k ) .
natgeh
Definition natgehtogehs ( n m : nat ) : n >= m -> S n >= m :=
natlehtolehs _ _ .
Definition natgehplusnmm ( n m : nat ) : n + m >= m :=
negnatgthmplusnm _ _ .
Definition natgehplusnmn ( n m : nat ) : n + m >= n :=
negnatgthnplusnm _ _ .
Definition natgehandplusl ( n m k : nat ) : n >= m -> k + n >= k + m :=
negf ( natgthandpluslinv m n k ) .
Definition natgehandplusr ( n m k : nat ) : n >= m -> n + k >= m + k :=
negf ( natgthandplusrinv m n k ) .
Definition natgehandpluslinv ( n m k : nat ) : k + n >= k + m -> n >= m :=
negf ( natgthandplusl m n k ) .
Definition natgehandplusrinv ( n m k : nat ) : n + k >= m + k -> n >= m :=
negf ( natgthandplusr m n k ) .
Definition natgthtogthp1 ( n m : nat ) : natgth n m -> natgth ( n + 1 ) m .
Proof. intros n m is . destruct (natpluscomm 1 n) . apply (natgthtogths n m is). Defined.
Definition natlthtolthp1 ( n m : nat ) : natlth n m -> natlth n ( m + 1 ) := natgthtogthp1 _ _ .
Definition natlehtolehp1 ( n m : nat ) : natleh n m -> natleh n ( m + 1 ) .
Proof . intros n m is . destruct (natpluscomm 1 m) . apply (natlehtolehs n m is). Defined.
Definition natgehtogehp1 ( n m : nat ) : natgeh n m -> natgeh ( n + 1 ) m := natlehtolehp1 _ _ .
Lemma natgthtogehp1 ( n m : nat ) : natgth n m -> natgeh n ( m + 1 ) .
Proof. intros n m is . destruct (natpluscomm 1 m) . apply (natgthtogehsn n m is). Defined .
Lemma natgthp1togeh ( n m : nat ) : natgth ( n + 1 ) m -> natgeh n m .
Proof. intros n m is . destruct (natpluscomm 1 n) . apply ( natgthsntogeh n m is). Defined.
Lemma natlehp1tolth ( n m : nat ) : natleh ( n + 1 ) m -> natlth n m .
Proof. intros n m is . destruct (natpluscomm 1 n) . apply (natlehsntolth n m is). Defined .
Lemma natlthtolehp1 ( n m : nat ) : natlth n m -> natleh ( n + 1 ) m .
Proof. intros n m is . destruct (natpluscomm 1 n) . apply (natlthtolehsn n m is). Defined .
Lemma natlthp1toleh ( n m : nat ) : natlth n ( m + 1 ) -> natleh n m .
Proof. intros n m is . destruct (natpluscomm 1 m) . apply (natlthsntoleh n m is). Defined.
Lemma natgehp1togth ( n m : nat ) : natgeh n ( m + 1 ) -> natgth n m .
Proof. intros n m is . destruct (natpluscomm 1 m) . apply (natgehsntogth n m is). Defined .
Lemma natlehchoice3 ( n m : nat ) : natleh n m -> coprod ( natleh ( n + 1 ) m ) ( paths n m ) .
Proof . intros n m l . destruct ( natlehchoice n m l ) as [ l' | e ] . apply ( ii1 ( natlthtolehp1 _ _ l' ) ) . apply ( ii2 e ) . Defined .
Lemma natgehchoice3 ( n m : nat ) : natgeh n m -> coprod ( natgeh n ( m + 1 ) ) ( paths n m ) .
Proof . intros n m g . destruct ( natgehchoice n m g ) as [ g' | e ] . apply ( ii1 ( natgthtogehp1 _ _ g' ) ) . apply ( ii2 e ) . Defined .
Lemma natgthchoice3 ( n m : nat ) : natgth n m -> coprod ( natgth n ( m + 1 ) ) ( paths n ( m + 1 ) ) .
Proof. intros n m g . destruct ( natgehchoice _ _ ( natgthtogehp1 _ _ g ) ) as [ g' | e ] . apply ( ii1 g' ) . apply ( ii2 e ) . Defined .
Lemma natlthchoice3 ( n m : nat ) : natlth n m -> coprod ( natlth ( n + 1 ) m ) ( paths ( n + 1 ) m ) .
Proof. intros n m l . destruct ( natlehchoice _ _ ( natlthtolehp1 _ _ l ) ) as [ l' | e ] . apply ( ii1 l' ) . apply ( ii2 e ) . Defined .
Lemma pathsitertoplus ( n m : nat ) : paths ( iteration S n m ) ( n + m ) .
Proof. intros . induction n as [ | n IHn ] . apply idpath . simpl . apply ( maponpaths S IHn ) . Defined .
Lemma isinclnatplusr ( n : nat ) : isincl ( fun m : nat => m + n ) .
Proof. intro . induction n as [ | n IHn ] . apply ( isofhlevelfhomot 1 _ _ ( fun m : nat => pathsinv0 ( natplusr0 m ) ) ) . apply ( isofhlevelfweq 1 ( idweq nat ) ) . apply ( isofhlevelfhomot 1 _ _ ( fun m : nat => pathsinv0 ( natplusnsm m n ) ) ) . simpl . apply ( isofhlevelfgf 1 _ _ isinclS IHn ) . Defined.
Lemma isinclnatplusl ( n : nat ) : isincl ( fun m : nat => n + m ) .
Proof. intro . apply ( isofhlevelfhomot 1 _ _ ( fun m : nat => natpluscomm m n ) ( isinclnatplusr n ) ) . Defined .
Lemma natplusrcan ( a b c : nat ) ( is : a + c = b + c ) : a = b .
Proof . intros . apply ( invmaponpathsincl _ ( isinclnatplusr c ) a b ) . apply is . Defined .
Lemma natpluslcan ( a b c : nat ) ( is : c + a = c + b ) : a = b .
Proof . intros . rewrite ( natpluscomm _ _ ) in is . rewrite ( natpluscomm c b ) in is . apply ( natplusrcan a b c is ) . Defined .
Lemma iscontrhfibernatplusr ( n m : nat ) ( is : natgeh m n ) : iscontr ( hfiber ( fun i : nat => i + n ) m ) .
Proof. intros . apply iscontraprop1 . apply isinclnatplusr . induction m as [ | m IHm ] . set ( e := natleh0tois0 _ is ) . split with 0 . apply e . destruct ( natlehchoice2 _ _ is ) as [ l | e ] . set ( j := IHm l ) . destruct j as [ j e' ] . split with ( S j ) . simpl . apply ( maponpaths S e' ) . split with 0 . simpl . assumption . Defined .
Lemma neghfibernatplusr ( n m : nat ) ( is : natlth m n ) : neg ( hfiber ( fun i : nat => i + n ) m ) .
Proof. intros. intro h . destruct h as [ i e ] . rewrite ( pathsinv0 e ) in is . destruct ( natlehtonegnatgth _ _ ( natlehmplusnm i n ) is ) . Defined .
Lemma isdecinclnatplusr ( n : nat ) : isdecincl ( fun i : nat => i + n ) .
Proof. intros . intro m . apply isdecpropif . apply ( isinclnatplusr _ m ) . destruct ( natlthorgeh m n ) as [ ni | i ] . apply ( ii2 ( neghfibernatplusr n m ni ) ) . apply ( ii1 ( pr1 ( iscontrhfibernatplusr n m i ) ) ) . Defined .
Some properties of minus on nat
Definition minuseq0 ( n m : nat ) ( is : n <= m ) : n - m = 0 .
Proof. intros n m . generalize n . clear n . induction m . intros n is . rewrite ( natleh0tois0 n is ) . simpl . apply idpath. intro n . destruct n . intro . apply idpath . apply (IHm n ) . Defined.
Definition minusgeh0 ( n m : nat ) ( is : n >= m ) : n - m >= 0 .
Proof. intro . induction n as [ | n IHn ] . intros. apply isreflnatgeh. intros .
apply natgehn0 . Defined.
Definition minusgth0 ( n m : nat ) ( is : n > m ) : n - m > 0.
Proof . intro n . induction n as [ | n IHn ] . intros . destruct (negnatgth0n _ is ) .
intro m . destruct m as [ | m ] . intro . apply natgthsn0 . intro is .
apply ( IHn m is ) . Defined.
Definition minusgth0inv ( n m : nat ) ( is : n - m > 0 ) : n > m .
Proof . intro . induction n as [ | n IHn ] . intros . destruct ( negnatgth0n _ is ) . intro . destruct m as [ | m ]. intros . apply natgthsn0. intro . apply ( IHn m is ) . Defined.
Definition natminuseqn ( n : nat ) : n - 0 = n .
Proof . intro. destruct n . apply idpath . apply idpath. Defined.
Definition natminuslehn ( n m : nat ) : n - m <= n .
Proof . intro n. induction n as [ | n IHn ] . intro. apply isreflnatleh .
intro . destruct m as [ | m ]. apply isreflnatleh . simpl .
apply ( istransnatleh _ _ _ (IHn m) ( natlehnsn n ) ) .
Defined.
Definition natminusgehn ( n m : nat ) : n >= n - m :=
natminuslehn _ _ .
Definition natminuslthn ( n m : nat ) ( is : n > 0 ) ( is' : m > 0 ) : n - m < n .
Proof . intro . induction n as [ | n IHn ] . intros . destruct ( negnatgth0n _ is ) . intro m . induction m . intros . destruct ( negnatgth0n _ is' ) . intros . apply ( natlehlthtrans _ n _ ) . apply ( natminuslehn n m ) . apply natlthnsn . Defined.
Definition natminuslthninv (n m : nat ) ( is : n - m < n ) : m > 0 .
Proof. intro . induction n as [ | n IHn ] . intros . destruct ( negnatlthn0 _ is ) . intro m . destruct m as [ | m ] . intro . destruct ( negnatlthnn _ is ) . intro . apply ( natgthsn0 m ) . Defined.
Definition minusplusnmm ( n m : nat ) ( is : n >= m ) : ( n - m ) + m = n .
Proof . intro n . induction n as [ | n IHn] . intro m . intro is . simpl . apply ( natleh0tois0 _ is ) . intro m . destruct m as [ | m ] . intro . simpl . rewrite ( natplusr0 n ) . apply idpath . simpl . intro is . rewrite ( natplusnsm ( n - m ) m ) . apply ( maponpaths S ( IHn m is ) ) . Defined .
Definition minusplusnmmineq ( n m : nat ) : ( n - m ) + m >= n .
Proof. intros. destruct ( natlthorgeh n m ) as [ lt | ge ] . rewrite ( minuseq0 _ _ ( natlthtoleh _ _ lt ) ). apply ( natgthtogeh _ _ lt ) . rewrite ( minusplusnmm _ _ ge ) . apply isreflnatgeh . Defined.
Definition plusminusnmm ( n m : nat ) : ( n + m ) - m = n .
Proof. intros . set ( int1 := natgehplusnmm n m ) . apply ( natplusrcan _ _ m ) . rewrite ( minusplusnmm _ _ int1 ) . apply idpath. Defined.
Definition natgehandminusr ( n m k : nat ) ( is : n >= m ) : n - k >= m - k .
Proof. intro n. induction n as [ | n IHn ] . intros . rewrite ( nat0gehtois0 _ is ) . apply isreflnatleh . intro m . induction m . intros . destruct k . apply natgehn0. apply natgehn0 . intro k . induction k . intro is . apply is . intro is . apply ( IHn m k is ) . Defined.
Definition natgehandminusl ( n m k : nat ) ( is : n >= m ) : n - k >= m - k .
Proof . intro n. induction n as [ | n IHn ] . intros . rewrite ( nat0gehtois0 _ is ) . apply isreflnatleh . intro m . induction m . intros . destruct k . apply natgehn0 . apply natgehn0 . intro k . induction k . intro is . apply is . intro is . apply ( IHn m k is ) . Defined.
Definition natgehandminusrinv ( n m k : nat ) ( is' : n >= k ) ( is : n - k >= m - k ) : n >= m .
Proof. intro n. induction n as [ | n IHn ] . intros . rewrite ( nat0gehtois0 _ is' ) in is . rewrite ( natminuseqn m ) in is . rewrite ( nat0gehtois0 _ is ) . apply isreflnatleh . intro m . induction m . intros . apply natgehn0 . intros . destruct k . rewrite natminuseqn in is . rewrite natminuseqn in is . apply is . apply ( IHn m k is' is ) . Defined.
Some properties of mult on nat
Basic algebraic properties of mult on nat
Lemma natmult0n ( n : nat ) : paths ( 0 * n ) 0 .
Proof. intro n . apply idpath . Defined .
Hint Resolve natmult0n : natarith .
Lemma natmultn0 ( n : nat ) : paths ( n * 0 ) 0 .
Proof. intro n . induction n as [ | n IHn ] . apply idpath . simpl . assumption . Defined .
Hint Resolve natmultn0 : natarith .
Lemma multsnm ( n m : nat ) : paths ( ( S n ) * m ) ( m + n * m ) .
Proof. intros . apply idpath . Defined .
Hint Resolve multsnm : natarith .
Lemma multnsm ( n m : nat ) : paths ( n * ( S m ) ) ( n + n * m ) .
Proof. intro n . induction n as [ | n IHn ] . intro . simpl . apply idpath . intro m . simpl . apply ( maponpaths S ) . rewrite ( pathsinv0 ( natplusassoc n m ( n * m ) ) ) . rewrite ( natpluscomm n m ) . rewrite ( natplusassoc m n ( n * m ) ) . apply ( maponpaths ( fun x : nat => m + x ) ( IHn m ) ) . Defined .
Hint Resolve multnsm : natarith .
Lemma natmultcomm ( n m : nat ) : paths ( n * m ) ( m * n ) .
Proof. intro . induction n as [ | n IHn ] . intro . auto with natarith . intro m . rewrite ( multsnm n m ) . rewrite ( multnsm m n ) . apply ( maponpaths ( fun x : _ => m + x ) ( IHn m ) ) . Defined .
Lemma natrdistr ( n m k : nat ) : paths ( ( n + m ) * k ) ( n * k + m * k ) .
Proof . intros . induction n as [ | n IHn ] . auto with natarith . simpl . rewrite ( natplusassoc k ( n * k ) ( m * k ) ) . apply ( maponpaths ( fun x : _ => k + x ) ( IHn ) ) . Defined .
Lemma natldistr ( m k n : nat ) : paths ( n * ( m + k ) ) ( n * m + n * k ) .
Proof . intros m k n . induction m as [ | m IHm ] . simpl . rewrite ( natmultn0 n ) . auto with natarith . simpl . rewrite ( multnsm n ( m + k ) ) . rewrite ( multnsm n m ) . rewrite ( natplusassoc _ _ _ ) . apply ( maponpaths ( fun x : _ => n + x ) ( IHm ) ) . Defined .
Lemma natmultassoc ( n m k : nat ) : paths ( ( n * m ) * k ) ( n * ( m * k ) ) .
Proof. intro . induction n as [ | n IHn ] . auto with natarith . intros . simpl . rewrite ( natrdistr m ( n * m ) k ) . apply ( maponpaths ( fun x : _ => m * k + x ) ( IHn m k ) ) . Defined .
Lemma natmultl1 ( n : nat ) : paths ( 1 * n ) n .
Proof. simpl . auto with natarith . Defined .
Hint Resolve natmultl1 : natarith .
Lemma natmultr1 ( n : nat ) : paths ( n * 1 ) n .
Proof. intro n . rewrite ( natmultcomm n 1 ) . auto with natarith . Defined .
Hint Resolve natmultr1 : natarith .
Definition natmultabmonoid : abmonoid := abmonoidpair ( setwithbinoppair natset ( fun n m : nat => n * m ) ) ( dirprodpair ( dirprodpair natmultassoc ( @isunitalpair natset _ 1 ( dirprodpair natmultl1 natmultr1 ) ) ) natmultcomm ) .
Definition natcommrig : commrig .
Proof . split with ( setwith2binoppair natset ( dirprodpair ( fun n m : nat => n + m ) ( fun n m : nat => n * m ) ) ) . split . split . split with ( dirprodpair ( dirprodpair ( dirprodpair natplusassoc ( @isunitalpair natset _ 0 ( dirprodpair natplusl0 natplusr0 ) ) ) natpluscomm ) ( dirprodpair natmultassoc ( @isunitalpair natset _ 1 ( dirprodpair natmultl1 natmultr1 ) ) ) ) . apply ( dirprodpair natmult0n natmultn0 ) . apply ( dirprodpair natldistr natrdistr ) . unfold iscomm . apply natmultcomm . Defined .
Definition natneq0andmult ( n m : nat ) ( isn : natneq n 0 ) ( ism : natneq m 0 ) : natneq ( n * m ) 0 .
Proof . intros . destruct n as [ | n ] . destruct ( isn ( idpath _ ) ) . destruct m as [ | m ] . destruct ( ism ( idpath _ ) ) . simpl . apply ( negpathssx0 ) . Defined .
Definition natneq0andmultlinv ( n m : nat ) ( isnm : natneq ( n * m ) 0 ) : natneq n 0 := rigneq0andmultlinv natcommrig n m isnm .
Definition natneq0andmultrinv ( n m : nat ) ( isnm : natneq ( n * m ) 0 ) : natneq m 0 := rigneq0andmultrinv natcommrig n m isnm .
Definition natgthandmultl ( n m k : nat ) ( is : natneq k 0 ) : natgth n m -> natgth ( k * n ) ( k * m ) .
Proof. intro n . induction n as [ | n IHn ] . intros m k g g' . destruct ( negnatgth0n _ g' ) . intro m . destruct m as [ | m ] . intros k g g' . rewrite ( natmultn0 k ) . rewrite ( multnsm k n ) . apply ( natgehgthtrans _ _ _ ( natgehplusnmn k ( k* n ) ) ( natneq0togth0 _ g ) ) . intros k g g' . rewrite ( multnsm k n ) . rewrite ( multnsm k m ) . apply ( natgthandplusl _ _ _ ) . apply ( IHn m k g g' ) . Defined .
Definition natgthandmultr ( n m k : nat ) ( is : natneq k 0 ) : natgth n m -> natgth ( n * k ) ( m * k ) .
Proof . intros n m k l . rewrite ( natmultcomm n k ) . rewrite ( natmultcomm m k ) . apply ( natgthandmultl n m k l ) . Defined .
Definition natgthandmultlinv ( n m k : nat ) : natgth ( k * n ) ( k * m ) -> natgth n m .
Proof . intro n . induction n as [ | n IHn ] . intros m k g . rewrite ( natmultn0 k ) in g . destruct ( negnatgth0n _ g ) . intro m . destruct m as [ | m ] . intros . apply ( natgthsn0 _ ) . intros k g . rewrite ( multnsm k n ) in g . rewrite ( multnsm k m ) in g . apply ( IHn m k ( natgthandpluslinv _ _ k g ) ) . Defined .
Definition natgthandmultrinv ( n m k : nat ) : natgth ( n * k ) ( m * k ) -> natgth n m .
Proof. intros n m k g . rewrite ( natmultcomm n k ) in g . rewrite ( natmultcomm m k ) in g . apply ( natgthandmultlinv n m k g ) . Defined .
natlth
Definition natlthandmultl ( n m k : nat ) ( is : natneq k 0 ) : natlth n m -> natlth ( k * n ) ( k * m ) := natgthandmultl _ _ _ is .
Definition natlthandmultr ( n m k : nat ) ( is : natneq k 0 ) : natlth n m -> natlth ( n * k ) ( m * k ) := natgthandmultr _ _ _ is .
Definition natlthandmultlinv ( n m k : nat ) : natlth ( k * n ) ( k * m ) -> natlth n m := natgthandmultlinv _ _ _ .
Definition natlthandmultrinv ( n m k : nat ) : natlth ( n * k ) ( m * k ) -> natlth n m := natgthandmultrinv _ _ _ .
natleh
Definition natlehandmultl ( n m k : nat ) : natleh n m -> natleh ( k * n ) ( k * m ) := negf ( natgthandmultlinv _ _ _ ) .
Definition natlehandmultr ( n m k : nat ) : natleh n m -> natleh ( n * k ) ( m * k ) := negf ( natgthandmultrinv _ _ _ ) .
Definition natlehandmultlinv ( n m k : nat ) ( is : natneq k 0 ) : natleh ( k * n ) ( k * m ) -> natleh n m := negf ( natgthandmultl _ _ _ is ) .
Definition natlehandmultrinv ( n m k : nat ) ( is : natneq k 0 ) : natleh ( n * k ) ( m * k ) -> natleh n m := negf ( natgthandmultr _ _ _ is ) .
natgeh
Definition natgehandmultl ( n m k : nat ) : natgeh n m -> natgeh ( k * n ) ( k * m ) := negf ( natgthandmultlinv _ _ _ ) .
Definition natgehandmultr ( n m k : nat ) : natgeh n m -> natgeh ( n * k ) ( m * k ) := negf ( natgthandmultrinv _ _ _ ) .
Definition natgehandmultlinv ( n m k : nat ) ( is : natneq k 0 ) : natgeh ( k * n ) ( k * m ) -> natgeh n m := negf ( natgthandmultl _ _ _ is ) .
Definition natgehandmultrinv ( n m k : nat ) ( is : natneq k 0 ) : natgeh ( n * k ) ( m * k ) -> natgeh n m := negf ( natgthandmultr _ _ _ is ) .
Open Scope rig_scope.
natgth
Lemma isplushrelnatgth : @isbinophrel nataddabmonoid natgth .
Proof . split . apply natgthandplusl . apply natgthandplusr . Defined .
Lemma isinvplushrelnatgth : @isinvbinophrel nataddabmonoid natgth .
Proof . split . apply natgthandpluslinv . apply natgthandplusrinv . Defined .
Lemma isinvmulthrelnatgth : @isinvbinophrel natmultabmonoid natgth .
Proof . split . intros a b c r . apply ( natlthandmultlinv _ _ _ r ) . intros a b c r . apply ( natlthandmultrinv _ _ _ r ) . Defined .
Lemma isrigmultgtnatgth : isrigmultgt natcommrig natgth .
Proof . change ( forall a b c d : nat , natgth a b -> natgth c d -> natgth ( a * c + b * d ) ( a * d + b * c ) ) . intro a . induction a as [ | a IHa ] . intros b c d rab rcd . destruct ( negnatgth0n _ rab ) .
intro b . induction b as [ | b IHb ] . intros c d rab rcd . rewrite ( natmult0n d ) . rewrite ( natplusr0 _ ) . rewrite ( natmult0n _ ) . rewrite ( natplusr0 _ ) . apply ( natlthandmultl _ _ _ ( natgthtoneq _ _ rab ) rcd ) . intros c d rab rcd . simpl . set ( rer := ( abmonoidrer nataddabmonoid ) ) . simpl in rer . rewrite ( rer _ _ d _ ) . rewrite ( rer _ _ c _ ) . rewrite ( natpluscomm c d ) . apply ( natlthandplusl (a * d + b * c) (a * c + b * d) ( d + c ) ) . apply ( IHa _ _ _ rab rcd ) . Defined .
Lemma isinvrigmultgtnatgth : isinvrigmultgt natcommrig natgth .
Proof . set ( rer := abmonoidrer nataddabmonoid ) . simpl in rer . apply isinvrigmultgtif . intros a b c d . generalize a b c . clear a b c . induction d as [ | d IHd ] .
intros a b c g gab . change ( pr1 ( natgth ( a * c + b * 0 ) ( a * 0 + b * c ) ) ) in g . destruct c as [ | c ] . rewrite ( natmultn0 _ ) in g . destruct ( isirreflnatgth _ g ) . apply natgthsn0 .
intros a b c g gab . destruct c as [ | c ] . change ( pr1 ( natgth ( a * 0 + b * S d ) ( a * S d + b * 0 ) ) ) in g . rewrite ( natmultn0 _ ) in g . rewrite ( natmultn0 _ ) in g . rewrite ( natplusl0 _ ) in g . rewrite ( natplusr0 _ ) in g . set ( g' := natgthandmultrinv _ _ _ g ) . destruct ( isasymmnatgth _ _ gab g' ) . change ( pr1 ( natgth ( a * S c + b * S d ) ( a * S d + b * S c ) ) ) in g . rewrite ( multnsm _ _ ) in g . rewrite ( multnsm _ _ ) in g . rewrite ( multnsm _ _ ) in g . rewrite ( multnsm _ _ ) in g . rewrite ( rer _ ( a * c ) _ _ ) in g . rewrite ( rer _ ( a * d ) _ _ ) in g . set ( g' := natgthandpluslinv _ _ ( a + b ) g ) . apply ( IHd a b c g' gab ) . Defined .
natlth
Lemma isplushrelnatlth : @isbinophrel nataddabmonoid natlth .
Proof . split . intros a b c . apply ( natgthandplusl b a c ) . intros a b c . apply ( natgthandplusr b a c ) . Defined .
Lemma isinvplushrelnatlth : @isinvbinophrel nataddabmonoid natlth .
Proof . split . intros a b c . apply ( natgthandpluslinv b a c ) . intros a b c . apply ( natgthandplusrinv b a c ) . Defined .
Lemma isinvmulthrelnatlth : @isinvbinophrel natmultabmonoid natlth .
Proof . split . intros a b c r . apply ( natlthandmultlinv _ _ _ r ) . intros a b c r . apply ( natlthandmultrinv _ _ _ r ) . Defined .
natleh
Lemma isplushrelnatleh : @isbinophrel nataddabmonoid natleh .
Proof . split . apply natlehandplusl . apply natlehandplusr . Defined .
Lemma isinvplushrelnatleh : @isinvbinophrel nataddabmonoid natleh .
Proof . split . apply natlehandpluslinv . apply natlehandplusrinv . Defined .
Lemma ispartinvmulthrelnatleh : @ispartinvbinophrel natmultabmonoid ( fun x => natneq x 0 ) natleh .
Proof . split . intros a b c s r . apply ( natlehandmultlinv _ _ _ s r ) . intros a b c s r . apply ( natlehandmultrinv _ _ _ s r ) . Defined .
natgeh
Lemma isplushrelnatgeh : @isbinophrel nataddabmonoid natgeh .
Proof . split . intros a b c . apply ( natlehandplusl b a c ) . intros a b c . apply ( natlehandplusr b a c ) . Defined .
Lemma isinvplushrelnatgeh : @isinvbinophrel nataddabmonoid natgeh .
Proof . split . intros a b c . apply ( natlehandpluslinv b a c ) . intros a b c . apply ( natlehandplusrinv b a c ) . Defined .
Lemma ispartinvmulthrelnatgeh : @ispartinvbinophrel natmultabmonoid ( fun x => natneq x 0 ) natgeh .
Proof . split . intros a b c s r . apply ( natlehandmultlinv _ _ _ s r ) . intros a b c s r . apply ( natlehandmultrinv _ _ _ s r ) . Defined .
Close Scope rig_scope .
Definition natnonzero : @subabmonoids natmultabmonoid .
Proof . split with ( fun a => natneq a 0 ) . unfold issubmonoid . split . unfold issubsetwithbinop . intros a a' . apply ( natneq0andmult _ _ ( pr2 a ) ( pr2 a' ) ) . apply ( ct ( natneq , isdecrelnatneq, 1 , 0 ) ) . Defined .
Lemma natnonzerocomm ( a b : natnonzero ) : paths ( @op natnonzero a b ) ( @op natnonzero b a ) .
Proof . intros . apply ( invmaponpathsincl _ ( isinclpr1carrier _ ) ( @op natnonzero a b ) ( @op natnonzero b a ) ) . simpl . apply natmultcomm . Defined .
Division with a remainder on nat
Definition natdivrem ( n m : nat ) : dirprod nat nat .
Proof. intros . induction n as [ | n IHn ] . intros . apply ( dirprodpair 0 0 ) . destruct ( natlthorgeh ( S ( pr2 IHn ) ) m ) . apply ( dirprodpair ( pr1 IHn ) ( S ( pr2 IHn ) ) ) . apply ( dirprodpair ( S ( pr1 IHn ) ) 0 ) . Defined .
Definition natdiv ( n m : nat ) := pr1 ( natdivrem n m ) .
Definition natrem ( n m : nat ) := pr2 ( natdivrem n m ) .
Lemma lthnatrem ( n m : nat ) ( is : natneq m 0 ) : natlth ( natrem n m ) m .
Proof. intro . destruct n as [ | n ] . unfold natrem . simpl . intros. apply ( natneq0togth0 _ is ) . unfold natrem . intros m is . simpl . destruct ( natlthorgeh (S (pr2 (natdivrem n m))) m ) as [ nt | t ] . simpl . apply nt . simpl . apply ( natneq0togth0 _ is ) . Defined .
Theorem natdivremrule ( n m : nat ) ( is : natneq m 0 ) : paths n ( ( natrem n m ) + ( natdiv n m ) * m ) .
Proof. intro . induction n as [ | n IHn ] . simpl . intros . apply idpath . intros m is . unfold natrem . unfold natdiv . simpl . destruct ( natlthorgeh ( S ( pr2 ( natdivrem n m ) ) ) m ) as [ nt | t ] .
simpl . apply ( maponpaths S ( IHn m is ) ) .
simpl . set ( is' := lthnatrem n m is ) . destruct ( natgthchoice2 _ _ is' ) as [ h | e ] . destruct ( natlehtonegnatgth _ _ t h ) . fold ( natdiv n m ) . set ( e'' := maponpaths S ( IHn m is ) ) . change (S (natrem n m + natdiv n m * m) ) with ( S ( natrem n m ) + natdiv n m * m ) in e'' . rewrite ( pathsinv0 e ) in e'' . apply e'' .
Defined .
Opaque natdivremrule .
Lemma natlehmultnatdiv ( n m : nat ) ( is : natneq m 0 ) : natleh ( mult ( natdiv n m ) m ) n .
Proof . intros . set ( e := natdivremrule n m ) . set ( int := ( natdiv n m ) * m ) . rewrite e . unfold int . apply ( natlehmplusnm _ _ ) . apply is . Defined .
Theorem natdivremunique ( m i j i' j' : nat ) ( lj : natlth j m ) ( lj' : natlth j' m ) ( e : paths ( j + i * m ) ( j' + i' * m ) ) : dirprod ( paths i i' ) ( paths j j' ) .
Proof. intros m i . induction i as [ | i IHi ] .
intros j i' j' lj lj' . intro e . simpl in e . rewrite ( natplusr0 j ) in e . rewrite e in lj . destruct i' . simpl in e . rewrite ( natplusr0 j' ) in e . apply ( dirprodpair ( idpath _ ) e ) . simpl in lj . rewrite ( natpluscomm m ( i' * m ) ) in lj . rewrite ( pathsinv0 ( natplusassoc _ _ _ ) ) in lj . destruct ( negnatgthmplusnm _ _ lj ) .
intros j i' j' lj lj' e . destruct i' as [ | i' ] . simpl in e . rewrite ( natplusr0 j' ) in e . rewrite ( pathsinv0 e ) in lj' . rewrite ( natpluscomm m ( i * m ) ) in lj' . rewrite ( pathsinv0 ( natplusassoc _ _ _ ) ) in lj' . destruct ( negnatgthmplusnm _ _ lj' ) .
simpl in e . rewrite ( natpluscomm m ( i * m ) ) in e . rewrite ( natpluscomm m ( i' * m ) ) in e . rewrite ( pathsinv0 ( natplusassoc j _ _ ) ) in e . rewrite ( pathsinv0 ( natplusassoc j' _ _ ) ) in e . set ( e' := invmaponpathsincl _ ( isinclnatplusr m ) _ _ e ) . set ( ee := IHi j i' j' lj lj' e' ) . apply ( dirprodpair ( maponpaths S ( pr1 ee ) ) ( pr2 ee ) ) . Defined .
Opaque natdivremunique .
Lemma natdivremandmultl ( n m k : nat ) ( ism : natneq m 0 ) ( iskm : natneq ( k * m ) 0 ) : dirprod ( paths ( natdiv ( k * n ) ( k * m ) ) ( natdiv n m ) ) ( paths ( natrem ( k * n ) ( k * m ) ) ( k * ( natrem n m ) ) ) .
Proof . intros . set ( ak := natdiv ( k * n ) ( k * m ) ) . set ( bk := natrem ( k * n ) ( k * m ) ) . set ( a := natdiv n m ) . set ( b := natrem n m ) . assert ( e1 : paths ( bk + ak * ( k * m ) ) ( ( b * k ) + a * ( k * m ) ) ) . unfold ak. unfold bk . rewrite ( pathsinv0 ( natdivremrule ( k * n ) ( k * m ) iskm ) ) . rewrite ( natmultcomm k m ) . rewrite ( pathsinv0 ( natmultassoc _ _ _ ) ) . rewrite ( pathsinv0 ( natrdistr _ _ _ ) ) . unfold a . unfold b . rewrite ( pathsinv0 ( natdivremrule n m ism ) ) . apply ( natmultcomm k n ) . assert ( l1 := lthnatrem n m ism ) . assert ( l1' := ( natlthandmultr _ _ _ ( natneq0andmultlinv _ _ iskm ) l1 ) ) . rewrite ( natmultcomm m k ) in l1' . set ( int := natdivremunique _ _ _ _ _ ( lthnatrem ( k * n ) ( k * m ) iskm ) l1' e1 ) .
split with ( pr1 int ) .
rewrite ( natmultcomm k b ) . apply ( pr2 int ) . Defined .
Opaque natdivremandmultl .
Definition natdivandmultl ( n m k : nat ) ( ism : natneq m 0 ) ( iskm : natneq ( k * m ) 0 ) : paths ( natdiv ( k * n ) ( k * m ) ) ( natdiv n m ) := pr1 ( natdivremandmultl _ _ _ ism iskm ) .
Definition natremandmultl ( n m k : nat ) ( ism : natneq m 0 ) ( iskm : natneq ( k * m ) 0 ) : paths ( natrem ( k * n ) ( k * m ) ) ( k * ( natrem n m ) ) := pr2 ( natdivremandmultl _ _ _ ism iskm ) .
Lemma natdivremandmultr ( n m k : nat ) ( ism : natneq m 0 ) ( ismk : natneq ( m * k ) 0 ) : dirprod ( paths ( natdiv ( n * k ) ( m * k ) ) ( natdiv n m ) ) ( paths ( natrem ( n * k ) ( m * k) ) ( ( natrem n m ) * k ) ) .
Proof . intros . rewrite ( natmultcomm m k ) . rewrite ( natmultcomm m k ) in ismk . rewrite ( natmultcomm n k ) . rewrite ( natmultcomm ( natrem _ _ ) k ) . apply ( natdivremandmultl _ _ _ ism ismk ) . Defined .
Opaque natdivremandmultr .
Definition natdivandmultr ( n m k : nat ) ( ism : natneq m 0 ) ( ismk : natneq ( m * k ) 0 ) : paths ( natdiv ( n * k ) ( m * k ) ) ( natdiv n m ) := pr1 ( natdivremandmultr _ _ _ ism ismk ) .
Definition natremandmultr ( n m k : nat ) ( ism : natneq m 0 ) ( ismk : natneq ( m * k ) 0 ) : paths ( natrem ( n * k ) ( m * k ) ) ( ( natrem n m ) * k ) := pr2 ( natdivremandmultr _ _ _ ism ismk ) .
Fixpoint natpower ( n m : nat ) := match m with
O => 1 |
S m' => n * ( natpower n m' ) end .
Fixpoint factorial ( n : nat ) := match n with
0 => 1 |
S n' => ( S n' ) * ( factorial n' ) end .
Definition di ( i : nat ) ( x : nat ) : nat :=
match natlthorgeh x i with
ii1 _ => x |
ii2 _ => S x
end .
Lemma natlehdinsn ( i n : nat ) : natleh ( di i n ) ( S n ) .
Proof . intros . unfold di . destruct ( natlthorgeh n i ) . apply natlthtoleh . apply natlthnsn . apply isreflnatleh . Defined .
Lemma natgehdinn ( i n : nat ) : natgeh ( di i n ) n .
Proof. intros . unfold di . destruct ( natlthorgeh n i ) . apply isreflnatleh . apply natlthtoleh . apply natlthnsn . Defined .
Lemma isincldi ( i : nat ) : isincl ( di i ) .
Proof. intro . apply ( isinclbetweensets ( di i ) isasetnat isasetnat ) . intros x x' . unfold di . intro e. destruct ( natlthorgeh x i ) as [ l | nel ] . destruct ( natlthorgeh x' i ) as [ l' | nel' ] . apply e . rewrite e in l . set ( e' := natgthtogths _ _ l ) . destruct ( nel' e' ) . destruct ( natlthorgeh x' i ) as [ l' | nel' ] . destruct e. set ( e' := natgthtogths _ _ l' ) . destruct ( nel e' ) . apply ( invmaponpathsS _ _ e ) . Defined .
Lemma neghfiberdi ( i : nat ) : neg ( hfiber ( di i ) i ) .
Proof. intros i hf . unfold di in hf . destruct hf as [ j e ] . destruct ( natlthorgeh j i ) as [ l | g ] . destruct e . apply ( isirreflnatlth _ l) . destruct e in g . apply ( negnatgehnsn _ g ) . Defined.
Lemma iscontrhfiberdi ( i j : nat ) ( ne : neg ( paths i j ) ) : iscontr ( hfiber ( di i ) j ) .
Proof. intros . apply iscontraprop1 . apply ( isincldi i j ) . destruct ( natlthorgeh j i ) as [ l | nel ] . split with j . unfold di . destruct ( natlthorgeh j i ) as [ l' | nel' ] . apply idpath . destruct ( nel' l ) . destruct ( natgehchoice2 _ _ nel ) as [ g | e ] . destruct j as [ | j ] . destruct ( negnatgeh0sn _ g ) . split with j . unfold di . destruct ( natlthorgeh j i ) as [ l' | g' ] . destruct ( g l' ) . apply idpath . destruct ( ne ( pathsinv0 e ) ) . Defined .
Lemma isdecincldi ( i : nat ) : isdecincl ( di i ) .
Proof. intro i . intro j . apply isdecpropif . apply ( isincldi i j ) . destruct ( isdeceqnat i j ) as [ eq | neq ] . destruct eq . apply ( ii2 ( neghfiberdi i ) ) . apply ( ii1 ( pr1 ( iscontrhfiberdi i j neq ) ) ) . Defined .
Inductive types le with values in UU .
A generalization of le and its properties .
Inductive leF { T : UU } ( F : T -> T ) ( t : T ) : T -> UU := leF_O : leF F t t | leF_S : forall t' : T , leF F t t' -> leF F t ( F t' ) .
Lemma leFiter { T : UU } ( F : T -> T ) ( t : T ) ( n : nat ) : leF F t ( iteration F n t ) .
Proof. intros . induction n as [ | n IHn ] . apply leF_O . simpl . unfold funcomp . apply leF_S . assumption . Defined .
Lemma leFtototal2withnat { T : UU } ( F : T -> T ) ( t t' : T ) ( a : leF F t t' ) : total2 ( fun n : nat => paths ( iteration F n t ) t' ) .
Proof. intros. induction a as [ | b H0 IH0 ] . split with O . apply idpath . split with ( S ( pr1 IH0 ) ) . simpl . apply ( @maponpaths _ _ F ( iteration F ( pr1 IH0 ) t ) b ) . apply ( pr2 IH0 ) . Defined.
Lemma total2withnattoleF { T : UU } ( F : T -> T ) ( t t' : T ) ( a : total2 ( fun n : nat => paths ( iteration F n t ) t' ) ) : leF F t t' .
Proof. intros . destruct a as [ n e ] . destruct e . apply leFiter. Defined .
Lemma leFtototal2withnat_l0 { T : UU } ( F : T -> T ) ( t : T ) ( n : nat ) : paths ( leFtototal2withnat F t _ (leFiter F t n)) ( tpair _ n ( idpath (iteration F n t) ) ) .
Proof . intros . induction n as [ | n IHn ] . apply idpath . simpl .
set ( h := fun ne : total2 ( fun n0 : nat => paths ( iteration F n0 t ) ( iteration F n t ) ) => tpair ( fun n0 : nat => paths ( iteration F n0 t ) ( iteration F ( S n ) t ) ) ( S ( pr1 ne ) ) ( maponpaths F ( pr2 ne ) ) ) . apply ( @maponpaths _ _ h _ _ IHn ) . Defined.
Lemma isweqleFtototal2withnat { T : UU } ( F : T -> T ) ( t t' : T ) : isweq ( leFtototal2withnat F t t' ) .
Proof . intros . set ( f := leFtototal2withnat F t t' ) . set ( g := total2withnattoleF F t t' ) .
assert ( egf : forall x : _ , paths ( g ( f x ) ) x ) . intro x . induction x as [ | y H0 IHH0 ] . apply idpath . simpl . simpl in IHH0 . destruct (leFtototal2withnat F t y H0 ) as [ m e ] . destruct e . simpl . simpl in IHH0. apply ( @maponpaths _ _ ( leF_S F t (iteration F m t) ) _ _ IHH0 ) .
assert ( efg : forall x : _ , paths ( f ( g x ) ) x ) . intro x . destruct x as [ n e ] . destruct e . simpl . apply leFtototal2withnat_l0 .
apply ( gradth _ _ egf efg ) . Defined.
Definition weqleFtototalwithnat { T : UU } ( F : T -> T ) ( t t' : T ) : weq ( leF F t t' ) ( total2 ( fun n : nat => paths ( iteration F n t ) t' ) ) := weqpair _ ( isweqleFtototal2withnat F t t' ) .
Definition le ( n : nat ) : nat -> UU := leF S n .
Definition le_n := leF_O S .
Definition le_S := leF_S S .
Theorem isaprople ( n m : nat ) : isaprop ( le n m ) .
Proof. intros . apply ( isofhlevelweqb 1 ( weqleFtototalwithnat S n m ) ) . apply invproofirrelevance . intros x x' . set ( i := @pr1 _ (fun n0 : nat => paths (iteration S n0 n) m) ) . assert ( is : isincl i ) . apply ( isinclpr1 _ ( fun n0 : nat => isasetnat (iteration S n0 n) m ) ) . apply ( invmaponpathsincl _ is ) . destruct x as [ n1 e1 ] . destruct x' as [ n2 e2 ] . simpl . set ( int1 := pathsinv0 ( pathsitertoplus n1 n ) ) . set ( int2 := pathsinv0 (pathsitertoplus n2 n ) ) . set ( ee1 := pathscomp0 int1 e1 ) . set ( ee2 := pathscomp0 int2 e2 ) . set ( e := pathscomp0 ee1 ( pathsinv0 ee2 ) ) . apply ( invmaponpathsincl _ ( isinclnatplusr n ) n1 n2 e ) . Defined .
Lemma letoleh ( n m : nat ) : le n m -> natleh n m .
Proof . intros n m H . induction H as [ | m H0 IHH0 ] . apply isreflnatleh . apply natlehtolehs . assumption . Defined .
Lemma natlehtole ( n m : nat ) : natleh n m -> le n m .
Proof. intros n m H . induction m . assert ( int := natleh0tois0 n H ) . clear H . destruct int . apply le_n .
set ( int2 := natlehchoice2 n ( S m ) H ) . destruct int2 as [ isnatleh | iseq ] . apply ( le_S n m ( IHm isnatleh ) ) . destruct iseq . apply le_n . Defined .
Lemma isweqletoleh ( n m : nat ) : isweq ( letoleh n m ) .
Proof. intros . set ( is1 := isaprople n m ) . set ( is2 := pr2 ( natleh n m ) ) . apply ( isweqimplimpl ( letoleh n m ) ( natlehtole n m ) is1 is2 ) . Defined .
Definition weqletoleh ( n m : nat ) := weqpair _ ( isweqletoleh n m ) .