proposition: Lemma fib_satisfies_other_equation : fib (=) Cons 0 (Cons 1 (pointwise_plus (tl fib) fib)).
proof: Proof. apply trans_bisimilar with (Cons 0 (pointwise_plus_tl 1 fib fib));[apply fib_cofixed|]. constructor; trivial. apply trans_bisimilar with (pointwise_plus (Cons 1 fib) fib); [apply (pointwise_plus_pointwise_plus_tl 1 fib fib)|]. rewrite pointwise_plus_cofixed. constructor; [trivial|simpl; apply pointwise_plus_comm]. Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith