%% Results on co-natural numbers (natural numbers with infinity)
Kind conat type.
Type z conat.
Type s conat -> conat.
CoDefine conat : conat -> prop by
conat z ;
conat (s A) := conat A.
CoDefine coeq : conat -> conat -> prop by
coeq z z ;
coeq (s A) (s B) := coeq A B.
CoDefine inf : conat -> prop by
inf (s A) := inf A.
CoDefine coadd : conat -> conat -> conat -> prop by
coadd (s A) B (s C) := coadd A B C ;
coadd z (s B) (s C) := coadd z B C ;
coadd z z z.
Theorem coeq_refl : forall A,
conat A -> coeq A A.
coinduction. intros. case H1.
search.
apply CH to H2. search.
Theorem coeq_sym : forall A B,
coeq A B -> coeq B A.
coinduction. intros. case H1.
search.
apply CH to H2. search.
Theorem coeq_trans : forall A B C,
coeq A B -> coeq B C -> coeq A C.
coinduction. intros. case H1.
search.
case H2. apply CH to H3 H4. search.
Theorem inf_plus_one : forall A,
inf A -> coeq A (s A).
coinduction. intros. case H1.
apply CH to H2. search.
Theorem coadd_det : forall A B C D,
coadd A B C -> coadd A B D -> coeq C D.
coinduction. intros. case H1.
case H2. apply CH to H3 H4. search.
case H2. apply CH to H3 H4. search.
case H2. search.
Theorem coadd_z : forall A,
conat A -> coadd A z A.
coinduction. intros. case H1.
search.
apply CH to H2. search.
Theorem coadd_inf1 : forall A B C,
inf A -> coadd A B C -> inf C.
coinduction. intros. case H1.
case H2. apply CH to H3 H4. search.
Theorem coadd_inf2 : forall A B C,
conat A -> inf B -> coadd A B C -> inf C.
coinduction. intros. case H3.
case H1. apply CH to H5 H2 H4. search.
case H2. apply CH to H1 H5 H4. search.
search.
