I’m attempting to dip my toes into Coq’s coinduction facilities, and I have no idea where to start. While this topic is ostensibly about the conaturals, I welcome any and all suggestions for beginner-level tutorials on the subject of coinduction in Coq.

Consider the following development:

```
CoInductive conat: Set :=
| coz: conat
| cosucc: conat -> conat.
CoFixpoint omega: conat := cosucc omega.
Goal omega = cosucc omega.
Proof.
Fail reflexivity.
Abort.
Goal coz <> omega.
Proof.
intro H.
inversion H. (* does not accomplish any progress *)
Abort.
```

In *Certified Programming with Dependent Types* Adam Chlipala suggests the definition of an elaborate identity function (which he calls `frob`

) with an associated congruence lemma (`frob_eq`

), and using the later to rewrite the term. Is this truly the most straightforward way to proceed?

```
Definition frob (n: conat): conat :=
match n with
| coz => coz
| cosucc n => cosucc n
end.
Lemma frob_eq (n: conat): n = frob n.
Proof.
intros.
destruct n; reflexivity.
Qed.
Goal omega = cosucc omega.
Proof.
replace (omega = cosucc omega) with (frob omega = cosucc omega).
- reflexivity.
- rewrite <- frob_eq. reflexivity.
Qed.
Goal coz <> omega.
Proof.
rewrite (frob_eq omega).
simpl.
intro H; inversion H.
Qed.
```