Results on co-natural numbers (natural numbers with infinity)


[View conat.thm]

Click on a command or tactic to see a detailed view of its use.

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.

Theorem coeq_sym : forall A B,
  coeq A B -> coeq B A.

Theorem coeq_trans : forall A B C,
  coeq A B -> coeq B C -> coeq A C.

Theorem inf_plus_one : forall A,
  inf A -> coeq A (s A).

Theorem coadd_det : forall A B C D,
  coadd A B C -> coadd A B D -> coeq C D.

Theorem coadd_z : forall A,
  conat A -> coadd A z A.

Theorem coadd_inf1 : forall A B C,
  inf A -> coadd A B C -> inf C.

Theorem coadd_inf2 : forall A B C,
  conat A -> inf B -> coadd A B C -> inf C.