@Andrej Bauer has introduced a smarter definition of coadd and has proven that it is commutative.

However, I would like to show that we can prove commutativity without updating the definition of coadd.

The full proof can be found here

The proof involves natural numbers so I will update my notation to hopefully avoid confusion.

For example, S is replaced with CoS to avoid confusion with the successor constructor S for natural numbers.

Futhermore, I will be using n and m for CoNat and N for nat

The definitions from my question are updated as follows (note that only the notation has changed)

CoInductive CoNat :=
| CoZ : CoNat
| CoS : CoNat -> CoNat.

CoInductive bisimilar : CoNat -> CoNat -> Prop :=
| bisimilar_CoZ: bisimilar CoZ CoZ
| bisimilar_CoS: forall n m, bisimilar m n ->  bisimilar (CoS m) (CoS n).

Definition evalCoNat (n : CoNat) :=
  match n with
  | CoZ => CoZ
  | CoS n => CoS n
  end.

CoFixpoint coadd (m : CoNat) (n : CoNat) :=
  match m with
  | CoZ => n
  | CoS m' => CoS (coadd m' n)
  end.

from these definitions you are able to prove the following

bisim_reflexive: forall n: CoNat, bisimilar n n
bisim_symmetric: forall m n : CoNat, bisimilar m n -> bisimilar n m

(* These helped when rewriting *)
coadd_eq_CoZ : forall n, n = coadd CoZ n.
coadd_eq_CoS: forall m n, CoS (coadd m n) = coadd (CoS m) n.

bisimilar_coadd_n_CoZ: forall n, bisimilar (coadd n CoZ) n.

Now the trick I found was to introduce

Fixpoint succN (N: nat) (n : CoNat) :=
  match N with
  | O => n
  | S N' =>  CoS (succN N' n) 
  end.

If we are able to prove a more general lemma

Lemma bisimilar_m_succN_n_eq_n_succN_m:
  forall (m n : CoNat) (N : nat), bisimilar (coadd m (succN N n)) (coadd n (succN N m)).

then we can prove commutativity as it is a specific case of the lemma above, namely when N = 0. That proof is as follows,

Lemma bisimilar_coadd_comm: forall m n : CoNat, bisimilar (coadd m n) (coadd n m).
Proof.
  intros m n.
  specialize bisimilar_m_succN_n_eq_n_succN_m with (n:= n) (m:=m) (N:= O).
  auto.
Qed.

Before proving bisimilar_m_succN_n_eq_n_succN_m we need some auxilliary lemmas

(*  succN_eq_O and succN_eq_S helped when rewriting *)
Lemma succN_eq_O: forall n, n = succN O n.
Proof. intros n. reflexivity. Qed.

Lemma succN_eq_S: forall N n, CoS (succN N n) = succN (S N) n. 
Proof. intros N n. reflexivity. Qed.

Lemma succ_N_Cos_n_eq_succN_SN_n: forall N n,  succN N (CoS n) = succN (S N) n.
Proof.
  simpl.
  intros N n.
  induction N.
  - simpl. reflexivity.
  - simpl. rewrite IHN. reflexivity.
  Qed.

Now we have everything we need to prove bisimilar_m_succN_n_eq_n_succN_m

Lemma bisimilar_m_succN_n_eq_n_succN_m:
  forall (m n : CoNat) (N : nat), bisimilar (coadd m (succN N n)) (coadd n (succN N m)).
Proof. 
  cofix CIH.
  intros m n N.
  destruct N; destruct m; destruct n.
  - simpl. apply bisim_reflexive.
  - simpl. 
    rewrite evalCoNat_eq with (n:= coadd CoZ (CoS n)).  simpl.
    apply bisim_symmetric. apply bisimilar_coadd_n_CoZ.
  - simpl.
    rewrite evalCoNat_eq with (n:= coadd CoZ (CoS m)).  simpl.
    apply bisimilar_coadd_n_CoZ.
  - simpl.
    rewrite evalCoNat_eq with (n:= coadd (CoS m) (CoS n)). simpl.
    rewrite evalCoNat_eq with (n:= coadd (CoS n) (CoS m)). simpl.
    apply bisimilar_CoS.
    specialize CIH with (n:= n) (m:=m) (N:= S O).
    simpl in CIH.
    apply CIH.
  - simpl. apply bisim_reflexive.
  - rewrite evalCoNat_eq with (n:= coadd CoZ (succN (S N) (CoS n))).
    simpl (evalCoNat (coadd CoZ _)).
    rewrite succ_N_Cos_n_eq_succN_SN_n.
    rewrite evalCoNat_eq with (n:= coadd (CoS n) (succN (S N) CoZ)).
    simpl (evalCoNat (coadd (CoS n) _)).
    apply bisimilar_CoS.
    rewrite succN_eq_S.
    rewrite coadd_eq_CoZ with (n:= succN (S N) n).
    apply CIH.
  - rewrite evalCoNat_eq with (n:= coadd CoZ _).
    simpl (evalCoNat (coadd CoZ _)).
    rewrite succ_N_Cos_n_eq_succN_SN_n.
    rewrite evalCoNat_eq with (n:= coadd _ _).
    simpl (evalCoNat (coadd (CoS m) (succN (S N) CoZ))).
    apply bisimilar_CoS.
    rewrite succN_eq_S.
    rewrite coadd_eq_CoZ with (n:= succN (S N) m).
    apply CIH.
  - rewrite evalCoNat_eq with (n:= coadd (CoS m) (succN (S N) (CoS n))). simpl.
    rewrite evalCoNat_eq with (n:= coadd (CoS n) (CoS (succN N (CoS m)))). simpl.
    apply bisimilar_CoS.
    rewrite succ_N_Cos_n_eq_succN_SN_n.
    rewrite succ_N_Cos_n_eq_succN_SN_n.
    rewrite succN_eq_S.
    rewrite succN_eq_S.
    apply CIH.
Qed

I understand the names for lemmas and proofs are far from elegant. Any improvements will be appreciated!