Click on a command or tactic to see a detailed view of its use.
%% Results on co-natural numbers (natural numbers with infinity) CoDefine conat z. CoDefine conat (s A) := conat A. CoDefine coeq z z. CoDefine coeq (s A) (s B) := coeq A B. CoDefine inf (s A) := inf A. CoDefine coadd (s A) B (s C) := coadd A B C. CoDefine coadd z (s B) (s C) := coadd z B C. CoDefine coadd z z z. Theorem coeq_refl : forall A, conat A -> coeq A A. [Show Proof][Hide Proof] coinduction. intros. case H1. search. apply CH to H2. search. Theorem coeq_sym : forall A B, coeq A B -> coeq B A. [Show Proof][Hide Proof] 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. [Show Proof][Hide Proof] 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). [Show Proof][Hide Proof] 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. [Show Proof][Hide Proof] 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. [Show Proof][Hide Proof] 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. [Show Proof][Hide Proof] 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. [Show Proof][Hide Proof] coinduction. intros. case H3. case H1. apply CH to H5 H2 H4. search. case H2. apply CH to H1 H5 H4. search. search.