proposition: Lemma pointwise_plus_comm :forall xs ys, pointwise_plus xs ys (=) pointwise_plus ys xs.
proof: Proof. cofix. destruct xs as [x0 xs], ys as [y0 ys]. rewrite pointwise_plus_cofixed. replace (pointwise_plus (Cons y0 ys) (Cons x0 xs)) with (Cons (y0 + x0) (pointwise_plus ys xs)); [|symmetry ; apply pointwise_plus_cofixed]. constructor; simpl. auto with zarith. apply pointwise_plus_comm. Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith