Set Primitive Projections.

Require Import Lia.

CoInductive NatStream : Type :=
  mkStream {
      hd : nat
    ; tl : NatStream
    }.

CoInductive NatStream_eq (x y : NatStream) : Type :=
  mkEq {
      hd_eq : hd x = hd y
    ; tl_R  : NatStream_eq (tl x) (tl y)
    }.

Notation "x ≈ y" := (NatStream_eq x y) (at level 55, no associativity).

CoFixpoint addS (n : nat) (xs : NatStream) : NatStream :=
  {|
    hd := n + hd xs;
    tl := addS n (tl xs)
  |}.

CoFixpoint sumS (xs ys : NatStream) : NatStream :=
  {|
    hd := hd xs + hd ys;
    tl := sumS (tl xs) (tl ys)
  |}.

CoFixpoint ps (n : nat) (xs : NatStream) : NatStream :=
  {|
    hd := n;
    tl := ps (n + hd xs) (tl xs)
  |}.

Definition prefixSums (xs : NatStream) : NatStream := ps 0 xs.

CoFixpoint seq (n : nat) : NatStream :=
  {|
    hd := n;
    tl := seq (S n)
  |}.

Lemma ue42' : forall (n m : nat) (xs : NatStream),
    ps (m + n) (addS 1 xs) ≈ sumS (seq m) (ps n xs).
  cofix ue42'.
  intros.
  apply mkEq; cbn; auto.
  replace (m + n + S (hd xs)) with (S m + (n + hd xs)) by lia.
  apply (ue42' _ _ (tl xs)).
Qed.

Lemma ue42 : forall (xs : NatStream),
    prefixSums (addS 1 xs) ≈ sumS (seq 0) (prefixSums xs).
  exact (ue42' 0 0).
Qed.