Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Import Logic.lib.Coqlib.
Require Import Logic.lib.StrongInduction.
Require Import Logic.lib.Stream.SigStream.

Definition fin_stream {A: Type} (h: list A) : stream A.
(* Goal: stream A *)
  exists (fun n => nth_error h n).
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@nth_error A h y) (@None A) *)
  rewrite nth_error_None_iff in H0 |- *.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
  omega.
Defined.

Definition inf_stream {A: Type} (h: nat -> A) : stream A.
(* Goal: stream A *)
  exists (fun n => Some (h n)).
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: False *)
  congruence.
Defined.

Lemma fin_stream_fin {A: Type}: forall l: list A, is_fin_stream (fin_stream l).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @is_fin_stream A (@fin_stream A l) *)
  exists (length l).
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  simpl.
(* Goal: @eq (option A) (@nth_error A l (@length A l)) (@None A) *)
  rewrite nth_error_None_iff; auto.
Qed.

Lemma inf_stream_inf {A: Type}: forall f: nat -> A, is_inf_stream (inf_stream f).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros; hnf; intros.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  simpl.
(* Goal: False *)
  congruence.
Qed.

Lemma fin_stream_n_stream {A: Type}: forall l: list A, is_n_stream (length l) (fin_stream l).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @is_n_stream A n (@fstn_stream A n h) *)
  split.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    apply nth_error_None_iff; omega.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  + intros.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
    simpl.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    rewrite nth_error_None_iff; omega.
Qed.

Definition empty_stream {A: Type}: stream A := fin_stream nil.

Definition empty_stream_spec {A: Type}: forall n, @empty_stream A n = None.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  simpl.
(* Goal: @eq (option A) (@nth_error A (@nil A) n) (@None A) *)
  destruct n; auto.
Qed.

Lemma empty_stream_is_empty {A: Type}: is_empty_stream (@empty_stream A).
Proof.
(* Goal: @is_n_stream A n (@fstn_stream A n h) *)
  split.
  + apply empty_stream_spec.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
  + intros; omega.
Qed.

Program Definition stream_map {A B: Type} (f: A -> B) (h: stream A): stream B :=
  fun n => match h n return option B with
           | Some a => Some (f a)
           | None => None
           end.
Next Obligation.
(* Goal: @eq (option B) match @stream_get A h y with | Some a => @Some B (f a) | None => @None B end (@None B) *)
  pose proof proj2_sig h x y H.
(* Goal: @eq (option B) match @stream_get A h y with | Some a => @Some B (f a) | None => @None B end (@None B) *)
  change (proj1_sig h) with (stream_get h) in H1.
(* Goal: False *)
  destruct (h x), (h y); try congruence.
(* Goal: False *)
  specialize (H1 eq_refl); congruence.
Qed.

Lemma stream_map_spec {A B: Type}: forall (f: A -> B) (h: stream A) (n: nat),
  stream_map f h n =
  match h n return option B with
  | Some a => Some (f a)
  | None => None
  end.
Proof.
(* Goal: forall (f : forall _ : A, B) (h : stream A) (n : nat), @eq (option B) (@stream_get B (@stream_map A B f h) n) match @stream_get A h n with | Some a => @Some B (f a) | None => @None B end *)
  intros; simpl; auto.
Qed.

Lemma stream_map_empty_stream {A B: Type}: forall (f: A -> B),
  stream_map f empty_stream = empty_stream.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (stream B) (@stream_map A B f (@stream_app A h1 h2)) (@stream_app B (@stream_map A B f h1) (@stream_map A B f h2)) *)
  stream_extensionality n.
(* Goal: @eq (option B) (@stream_get B (@stream_map A B f (@empty_stream A)) n) (@stream_get B (@empty_stream B) n) *)
  rewrite stream_map_spec, !empty_stream_spec.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  auto.
Qed.

Lemma stream_map_n_stream {A B: Type}: forall (f: A -> B) (h: stream A) (n: nat),
  is_n_stream n h <-> is_n_stream n (stream_map f h).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: iff (@is_inf_stream A h) (@is_inf_stream B (@stream_map A B f h)) *)
  split; intro.
(* Goal: @is_n_stream A n (@fstn_stream A n h) *)
  + destruct H; split.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    - rewrite stream_map_spec, H; auto.
    - intros; specialize (H0 n' H1).
(* Goal: False *)
      destruct (h n') eqn:HH; rewrite stream_map_spec, HH; congruence.
(* Goal: @is_n_stream A n (@fstn_stream A n h) *)
  + destruct H; split.
(* Goal: False *)
    - destruct (h n) eqn:HH; rewrite stream_map_spec, HH in H; congruence.
    - intros; specialize (H0 n' H1).
(* Goal: False *)
      destruct (h n') eqn:HH; rewrite stream_map_spec, HH in H0; congruence.
Qed.

Lemma stream_map_inf_stream {A B: Type}: forall (f: A -> B) (h: stream A),
  is_inf_stream h <-> is_inf_stream (stream_map f h).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: iff (@is_inf_stream A h) (@is_inf_stream B (@stream_map A B f h)) *)
  split; intro.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  + hnf; intros.
(* Goal: not (@eq (option B) (@stream_get B (@stream_map A B f h) n) (@None B)) *)
    specialize (H n).
(* Goal: False *)
    destruct (h n) eqn:HH; rewrite stream_map_spec, HH; congruence.
  + hnf; intros; specialize (H n).
(* Goal: False *)
    destruct (h n) eqn:HH; rewrite stream_map_spec, HH in H; congruence.
Qed.

Lemma stream_map_fin_stream {A B: Type}: forall (f: A -> B) (h: stream A),
  is_fin_stream h <-> is_fin_stream (stream_map f h).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: iff (@is_fin_stream A h) (@is_fin_stream B (@stream_map A B f h)) *)
  rewrite !is_fin_stream_spec.
(* Goal: iff (@ex nat (fun n : nat => @is_n_stream A n h)) (@ex nat (fun n : nat => @is_n_stream B n (@stream_map A B f h))) *)
  apply Morphisms_Prop.ex_iff_morphism; intros ?.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  apply stream_map_n_stream; auto.
Qed.

Lemma stream_map_at_least_n_stream {A B: Type}: forall (f: A -> B) (h: stream A) (n: nat),
  is_at_least_n_stream n h <-> is_at_least_n_stream n (stream_map f h).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: iff (@is_at_least_n_stream A n h) (@is_at_least_n_stream B n (@stream_map A B f h)) *)
  rewrite !at_least_n_stream_spec.
(* Goal: iff (or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h)) (or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream B m (@stream_map A B f h)))) (@is_inf_stream B (@stream_map A B f h))) *)
  apply Morphisms_Prop.or_iff_morphism.
  + apply Morphisms_Prop.ex_iff_morphism; intro.
(* Goal: iff (and (le a n) (@is_n_stream A a h)) (and (le a n) (@is_n_stream B a (@stream_map A B f h))) *)
    apply Morphisms_Prop.and_iff_morphism; [reflexivity |].
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    apply stream_map_n_stream; auto.
  + apply stream_map_inf_stream; auto.
Qed.

Lemma stream_map_at_most_n_stream {A B: Type}: forall (f: A -> B) (h: stream A) (n: nat),
  is_at_most_n_stream n h <-> is_at_most_n_stream n (stream_map f h).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: iff (@is_at_most_n_stream A n h) (@is_at_most_n_stream B n (@stream_map A B f h)) *)
  rewrite !at_most_n_stream_spec.
(* Goal: iff (@ex nat (fun m : nat => and (le m n) (@is_n_stream A m h))) (@ex nat (fun m : nat => and (le m n) (@is_n_stream B m (@stream_map A B f h)))) *)
  apply Morphisms_Prop.ex_iff_morphism; intro.
(* Goal: iff (and (le a n) (@is_n_stream A a h)) (and (le a n) (@is_n_stream B a (@stream_map A B f h))) *)
  apply Morphisms_Prop.and_iff_morphism; [reflexivity |].
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  apply stream_map_n_stream; auto.
Qed.

Program Definition fstn_stream {A: Type} (n: nat) (h: stream A) : stream A :=
  fun m => if le_lt_dec n m then None else h m.
Next Obligation.
(* Goal: False *)
  destruct (le_lt_dec n x), (le_lt_dec n y); try congruence.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
  + omega.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
  + apply (stream_sound1 h x y); auto; omega.
Qed.

Definition skipn_stream {A: Type} (n: nat) (h: stream A) : stream A.
  exists (fun m => h (m + n)).
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A h (Init.Nat.add y n)) (@None A) *)
  revert H0; apply (stream_sound1 h).
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
  omega.
Defined.

Lemma fstn_stream_Some {A: Type}: forall n m (h: stream A), m < n -> (fstn_stream n h) m = h m.
Proof.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  intros; simpl.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
  destruct (le_lt_dec n m); auto; omega.
Qed.

Lemma fstn_stream_None {A: Type}: forall n m (h: stream A), n <= m -> (fstn_stream n h) m = None.
Proof.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  intros; simpl.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
  destruct (le_lt_dec n m); auto; omega.
Qed.

Lemma fstn_stream_is_n_stream {A: Type}: forall n (h: stream A),
  is_at_least_n_stream n h ->
  is_n_stream n (fstn_stream n h).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A h (Init.Nat.add m n)) (@stream_get A (@empty_stream A) m) *)
  hnf in H.
(* Goal: @is_n_stream A n (@fstn_stream A n h) *)
  split.
  + rewrite fstn_stream_None by auto; auto.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  + intros.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    rewrite fstn_stream_Some by omega.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    apply H; omega.
Qed.

Lemma fstn_stream_eq {A: Type}: forall n (h: stream A),
  is_at_most_n_stream n h ->
  fstn_stream n h = h.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A h (Init.Nat.add m n)) (@stream_get A (@empty_stream A) m) *)
  hnf in H.
(* Goal: @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  stream_extensionality m.
(* Goal: @eq (option A) (@stream_get A (@fstn_stream A n (@stream_app A h1 h2)) m) (@stream_get A h1 m) *)
  destruct (lt_dec m n).
  + rewrite fstn_stream_Some by omega; auto.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
  + rewrite fstn_stream_None by omega.
(* Goal: @eq (option A) (@None A) (@stream_get A h m) *)
    symmetry.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    apply (stream_sound1 h n m); auto; omega.
Qed.

Lemma fstn_stream_is_fin_stream {A: Type}: forall n (h: stream A),
  is_fin_stream (fstn_stream n h).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A (@stream_app A h (@empty_stream A)) n) (@stream_get A h n) *)
  destruct (at_most_n_stream_or_at_least_Sn_stream h n).
  + rewrite fstn_stream_eq by auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    eapply at_most_n_stream_is_fin_stream; eauto.
  + eapply at_most_n_stream_is_fin_stream.
    apply fstn_stream_is_n_stream.
    eapply at_least_n_stream_mono; [| eauto].
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    omega.
Qed.

(*
Lemma fstn_stream_is_n_stream_inf {A: Type}: forall m (h: stream A),
  is_inf_stream h ->
  is_n_stream m (fstn_stream m h).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @is_n_stream A n (@fstn_stream A n h) *)
  split.
  + rewrite fstn_stream_None by auto; auto.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  + intros.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    rewrite fstn_stream_Some by omega.
    apply H.
Qed.

Lemma fstn_stream_is_n_stream' {A: Type}: forall n m (h: stream A),
  n <= m ->
  is_n_stream n h ->
  is_n_stream n (fstn_stream m h).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A (@empty_stream A) (Init.Nat.sub n m)) (@stream_get A h n) *)
  destruct H0.
(* Goal: @is_n_stream A n (@fstn_stream A n h) *)
  split.
  + destruct (lt_dec n m).
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    - rewrite fstn_stream_Some by auto; auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    - rewrite fstn_stream_None by omega; auto.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  + intros.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    rewrite fstn_stream_Some by omega.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    apply H1; omega.
Qed.
*)
Lemma skipn_stream_spec {A: Type}: forall n m (h: stream A), (skipn_stream n h) m = h (m + n).
Proof.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  intros; simpl.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  auto.
Qed.

Lemma skipn_stream_empty {A: Type}: forall n (h: stream A),
  is_at_most_n_stream n h ->
  skipn_stream n h = empty_stream.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  stream_extensionality m.
(* Goal: @eq (option A) (@stream_get A (@skipn_stream A n (@stream_app A h1 h2)) m) (@stream_get A h2 m) *)
  rewrite skipn_stream_spec.
(* Goal: @eq (option A) (@stream_get A h (Init.Nat.add m n)) (@stream_get A (@empty_stream A) m) *)
  hnf in H.
  rewrite (stream_sound1 h n (m + n)) by (auto; omega).
(* Goal: @eq (option A) (@None A) (@stream_get A (@empty_stream A) m) *)
  rewrite empty_stream_spec.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  auto.
Qed.

Definition partial_stream_len {A: Type} (h: stream A) (n: nat): option nat :=
  match h n with
  | Some _ => None
  | None => Some
    ((fix f (m: nat): nat :=
       match h m with
       | Some _ => S m
       | None => match m with
                 | 0 => 0
                 | S m0 => f m0
                 end
       end) n)
  end.

Lemma partial_stream_len_mono1: forall {A: Type} (h: stream A) (x y: nat), x <= y -> partial_stream_len h y = None -> partial_stream_len h x = None.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option nat) (@partial_stream_len A h y) (@Some nat n) *)
  unfold partial_stream_len in *.
(* Goal: False *)
  destruct (h y) eqn:?H; try congruence.
(* Goal: @eq (option nat) match @stream_get A h x with | Some a => @None nat | None => @Some nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) x) end (@None nat) *)
  pose proof (stream_sound2 h x y H) as [? ?]; [eauto |].
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  rewrite H2; auto.
Qed.

Lemma partial_stream_len_mono2: forall {A: Type} (h: stream A) (x y n: nat), x <= y -> partial_stream_len h x = Some n -> partial_stream_len h y = Some n.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option nat) (@partial_stream_len A h y) (@Some nat n) *)
  unfold partial_stream_len in *.
(* Goal: False *)
  destruct (h x) eqn:?H; try congruence.
(* Goal: @eq (option nat) match @stream_get A h y with | Some a => @None nat | None => @Some nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) y) end (@Some nat n) *)
  pose proof (stream_sound1 h x y H H1).
(* Goal: @eq (option nat) match @stream_get A h y with | Some a => @None nat | None => @Some nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) y) end (@Some nat n) *)
  inversion H0.
(* Goal: @eq (option nat) match @stream_get A h y with | Some a => @None nat | None => @Some nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) y) end (@Some nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) x)) *)
  rewrite H2, H4; clear H0.
(* Goal: @eq (option nat) (@Some nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) m)) (@Some nat n) *)
  f_equal.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  revert n H4; induction H; intros; auto.
(* Goal: @eq nat match @stream_get A h (S m) with | Some a => S (S m) | None => (fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) m end n *)
  pose proof (stream_sound1 h x m H H1).
(* Goal: @eq nat match @stream_get A h (S m) with | Some a => S (S m) | None => (fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) m end n *)
  specialize (IHle H0 _ H4).
(* Goal: @eq nat match @stream_get A h (S m) with | Some a => S (S m) | None => (fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) m end n *)
  rewrite IHle; clear IHle.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  rewrite H2; auto.
Qed.

Lemma partial_stream_len_Some {A: Type}: forall (h: stream A) (n m: nat),
  n <= m ->
  is_n_stream n h ->
  partial_stream_len h m = Some n.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option nat) (@partial_stream_len A h m) (@None nat) *)
  unfold partial_stream_len.
(* Goal: @eq (option A) (@stream_get A (@empty_stream A) (Init.Nat.sub n m)) (@stream_get A h n) *)
  destruct H0.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  rewrite (stream_sound1 h n m H) by auto.
(* Goal: @eq (option nat) (@Some nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) m)) (@Some nat n) *)
  f_equal.
  remember (m - n) as d.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
  replace m with (d + n) by omega.
(* Goal: @eq nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) (Init.Nat.add d n)) n *)
  clear Heqd H m.
(* Goal: @eq nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) (Init.Nat.add d n)) n *)
  induction d.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct n; rewrite H0; auto.
(* Goal: @eq nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) n) (S n) *)
    specialize (H1 n (le_n _)).
(* Goal: @eq nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) n) (S n) *)
    destruct (h n) eqn:?H; [| congruence].
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct n; rewrite H; auto.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
    rewrite (stream_sound1 h n (S (d + n))) by (auto; omega).
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    auto.
Qed.

Lemma partial_stream_len_None {A: Type}: forall (h: stream A) (m: nat),
  is_at_least_n_stream (S m) h ->
  partial_stream_len h m = None.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option nat) (@partial_stream_len A h m) (@None nat) *)
  unfold partial_stream_len.
(* Goal: @eq (option nat) match @stream_get A h m with | Some a => @None nat | None => @Some nat ((fix f (m : nat) : nat := match @stream_get A h m with | Some a => S m | None => match m with | O => O | S m0 => f m0 end end) m) end (@None nat) *)
  specialize (H m (le_n _)).
(* Goal: False *)
  destruct (h m); auto; congruence.
Qed.

Program Definition stream_app {A: Type} (h1 h2: stream A): stream A :=
  fun n: nat =>
    match partial_stream_len h1 n return option A with
    | None => h1 n
    | Some m => h2 (n - m)
    end.
Next Obligation.
(* Goal: @eq (option A) match @partial_stream_len A h1 y with | Some m => @stream_get A h2 (Init.Nat.sub y m) | None => @stream_get A h1 y end (@None A) *)
  destruct (partial_stream_len h1 x) eqn:?H.
  + pose proof H1.
(* Goal: @eq (option A) match @partial_stream_len A h1 y with | Some m => @stream_get A h2 (Init.Nat.sub y m) | None => @stream_get A h1 y end (@None A) *)
    apply (partial_stream_len_mono2 h1 x y n) in H1; [| omega].
(* Goal: @eq (option A) match @partial_stream_len A h1 y with | Some m => @stream_get A h2 (Init.Nat.sub y m) | None => @stream_get A h1 y end (@None A) *)
    rewrite H1.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    apply (stream_sound1 h2 (x - n) (y - n)); auto.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    omega.
  + unfold partial_stream_len in H1.
(* Goal: @eq (option A) match @partial_stream_len A h1 y with | Some m => @stream_get A h2 (Init.Nat.sub y m) | None => @stream_get A h1 y end (@None A) *)
    rewrite H0 in H1.
(* Goal: False *)
    congruence.
Qed.

Lemma stream_app_spec1 {A: Type}: forall (h1 h2: stream A) (m: nat),
  is_at_least_n_stream (S m) h1 ->
  stream_app h1 h2 m = h1 m.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  simpl.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  rewrite partial_stream_len_None by auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  auto.
Qed.

Lemma stream_app_spec1' {A: Type}: forall (h1 h2: stream A) (m: nat) a,
  h1 m = Some a ->
  stream_app h1 h2 m = Some a.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  rewrite stream_app_spec1; auto.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  hnf; intros.
(* Goal: not (@eq (option A) (@stream_get A (h O) n') (@None A)) *)
  intro.
(* Goal: False *)
  rewrite (stream_sound1 h1 n' m) in H by (auto; omega).
(* Goal: False *)
  congruence.
Qed.

Lemma stream_app_spec2 {A: Type}: forall (h1 h2: stream A) (n m: nat),
  is_n_stream n h1 ->
  stream_app h1 h2 (m + n) = h2 m.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  simpl.
(* Goal: @eq (option A) match @partial_stream_len A h1 (Init.Nat.add m n) with | Some m0 => @stream_get A h2 (Init.Nat.sub (Init.Nat.add m n) m0) | None => @stream_get A h1 (Init.Nat.add m n) end (@stream_get A h2 m) *)
  erewrite partial_stream_len_Some; [| | eassumption]; [| omega].
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
  f_equal; omega.
Qed.

Lemma stream_app_empty_stream {A: Type}: forall (h: stream A),
  stream_app h empty_stream = h.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (stream B) (@stream_map A B f (@stream_app A h1 h2)) (@stream_app B (@stream_map A B f h1) (@stream_map A B f h2)) *)
  stream_extensionality n.
(* Goal: @eq (option A) (@stream_get A (@stream_app A h (@empty_stream A)) n) (@stream_get A h n) *)
  destruct (at_most_n_stream_or_at_least_Sn_stream h n).
  + rewrite at_most_n_stream_spec in H.
(* Goal: @eq (option B) (@stream_get B (@stream_map A B f (@stream_app A h1 h2)) n) (@stream_get B (@stream_app B (@stream_map A B f h1) (@stream_map A B f h2)) n) *)
    destruct H as [m [? ?]].
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    replace n with ((n - m) + m) at 1 by omega.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite (stream_app_spec2 _ _ m) by auto.
(* Goal: @eq (option A) (@stream_get A (@empty_stream A) (Init.Nat.sub n m)) (@stream_get A h n) *)
    destruct H0.
(* Goal: @eq (option A) (@stream_get A (@empty_stream A) (Init.Nat.sub n m)) (@stream_get A h n) *)
    rewrite (stream_sound1 h m n) by (auto; omega).
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite empty_stream_spec; auto.
  + apply stream_app_spec1; auto.
Qed.

Lemma stream_app_fstn_skipn {A: Type}: forall (h: stream A) (n: nat),
  stream_app (fstn_stream n h) (skipn_stream n h) = h.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (stream A) (@stream_app A (@fstn_stream A n h) (@skipn_stream A n h)) h *)
  destruct (at_most_n_stream_or_at_least_n_stream h n).
  + rewrite fstn_stream_eq by auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite skipn_stream_empty by auto.
(* Goal: @eq (stream A) (@stream_app A h (@empty_stream A)) h *)
    apply stream_app_empty_stream.
  + stream_extensionality m.
(* Goal: @eq (option A) (@stream_get A (@fstn_stream A n (@stream_app A h1 h2)) m) (@stream_get A h1 m) *)
    destruct (lt_dec m n).
    - rewrite stream_app_spec1.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
      * rewrite fstn_stream_Some by auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
        auto.
      * apply fstn_stream_is_n_stream in H.
(* Goal: @is_at_least_n_stream A (S m) h1 *)
        rewrite at_least_n_stream_spec; left; exists n.
(* Goal: and (ge n (S m)) (@is_n_stream A n h1) *)
        split; [omega | auto].
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    - replace m with ((m - n) + n) at 1 by omega.
(* Goal: @eq (option A) (@stream_get A (@stream_app A (@fstn_stream A n h) (@skipn_stream A n h)) (Init.Nat.add (Init.Nat.sub m n) n)) (@stream_get A h m) *)
      rewrite (stream_app_spec2 _ _ n).
(* Goal: @eq (option A) (@stream_get A (@skipn_stream A n (@stream_app A h1 h2)) m) (@stream_get A h2 m) *)
      * rewrite skipn_stream_spec.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
        f_equal; omega.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
      * apply fstn_stream_is_n_stream; auto.
Qed.

Lemma stream_map_stream_app {A B: Type}: forall (f: A -> B) (h1 h2: stream A),
  stream_map f (stream_app h1 h2) = stream_app (stream_map f h1) (stream_map f h2).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (stream B) (@stream_map A B f (@stream_app A h1 h2)) (@stream_app B (@stream_map A B f h1) (@stream_map A B f h2)) *)
  stream_extensionality n.
(* Goal: @eq (option B) (@stream_get B (@stream_map A B f (@stream_app A h1 h2)) n) (@stream_get B (@stream_app B (@stream_map A B f h1) (@stream_map A B f h2)) n) *)
  destruct (at_most_n_stream_or_at_least_Sn_stream h1 n).
  + rewrite at_most_n_stream_spec in H.
(* Goal: @eq (option B) (@stream_get B (@stream_map A B f (@stream_app A h1 h2)) n) (@stream_get B (@stream_app B (@stream_map A B f h1) (@stream_map A B f h2)) n) *)
    destruct H as [m [? ?]].
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    replace n with ((n - m) + m) by omega.
(* Goal: @eq (option B) match @stream_get A h1 n with | Some a => @Some B (f a) | None => @None B end (@stream_get B (@stream_map A B f h1) n) *)
    rewrite stream_map_spec.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite stream_app_spec2 by auto.
(* Goal: @eq (option B) match @stream_get A h2 (Init.Nat.sub n m) with | Some a => @Some B (f a) | None => @None B end (@stream_get B (@stream_app B (@stream_map A B f h1) (@stream_map A B f h2)) (Init.Nat.add (Init.Nat.sub n m) m)) *)
    rewrite stream_app_spec2 by (apply stream_map_n_stream; auto).
(* Goal: @eq (option B) match @stream_get A h1 n with | Some a => @Some B (f a) | None => @None B end (@stream_get B (@stream_map A B f h1) n) *)
    rewrite stream_map_spec.
(* Goal: @eq (option B) match @stream_get A h2 (Init.Nat.sub n m) with | Some a => @Some B (f a) | None => @None B end match @stream_get A h2 (Init.Nat.sub n m) with | Some a => @Some B (f a) | None => @None B end *)
    reflexivity.
  + rewrite stream_app_spec1 by (apply stream_map_at_least_n_stream; auto).
(* Goal: @eq (option B) match @stream_get A h1 n with | Some a => @Some B (f a) | None => @None B end (@stream_get B (@stream_map A B f h1) n) *)
    rewrite stream_map_spec.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite stream_app_spec1 by auto.
(* Goal: @eq (option B) match @stream_get A h1 n with | Some a => @Some B (f a) | None => @None B end (@stream_get B (@stream_map A B f h1) n) *)
    rewrite stream_map_spec.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    auto.
Qed.

Lemma stream_app_fstn_stream {A: Type}: forall (h1 h2: stream A) (n: nat),
  is_n_stream n h1 ->
  fstn_stream n (stream_app h1 h2) = h1.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  stream_extensionality m.
(* Goal: @eq (option A) (@stream_get A (@fstn_stream A n (@stream_app A h1 h2)) m) (@stream_get A h1 m) *)
  destruct (lt_dec m n).
  + rewrite fstn_stream_Some by auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite stream_app_spec1; auto.
(* Goal: @is_at_least_n_stream A (S m) h1 *)
    rewrite at_least_n_stream_spec; left; exists n.
(* Goal: and (ge n (S m)) (@is_n_stream A n h1) *)
    split; [omega | auto].
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
  + rewrite fstn_stream_None by omega.
(* Goal: @eq (option A) match match @stream_get A (h O) O with | Some a => @Some (prod nat nat) (@pair nat nat O O) | None => @None (prod nat nat) end with | Some (pair k m as p) => @stream_get A (h k) m | None => @None A end (@None A) *)
    destruct H as [? _].
(* Goal: @eq (option A) (@None A) (@stream_get A h1 m) *)
    rewrite (stream_sound1 h1 n m) by (auto; omega).
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    auto.
Qed.

Lemma stream_app_skipn_stream {A: Type}: forall (h1 h2: stream A) (n: nat),
  is_n_stream n h1 ->
  skipn_stream n (stream_app h1 h2) = h2.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  stream_extensionality m.
(* Goal: @eq (option A) (@stream_get A (@skipn_stream A n (@stream_app A h1 h2)) m) (@stream_get A h2 m) *)
  rewrite skipn_stream_spec.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  rewrite stream_app_spec2; auto.
Qed.

Fixpoint partial_stream_clen {A: Type} (h: nat -> stream A) (n: nat): nat * nat :=
  match n with
  | 0 => (0, 0)
  | S n => let (k, m) := partial_stream_clen h n in
           match h k (S m) with
           | Some _ => (k, S m)
           | None => (S k, 0)
           end
  end.

Fixpoint partial_stream_clen' {A: Type} (h: nat -> stream A) (n: nat): option (nat * nat) :=
  let (k, m) := partial_stream_clen h n in
  match n with
  | 0 => match h k m with
         | Some _ => Some (k, m)
         | None => None
         end
  | S n => match h k m, partial_stream_clen' h n with
           | Some _, Some _ => Some (k, m)
           | _, _ => None
           end
  end.

Lemma partial_stream_clen'_None_iff {A: Type}: forall (h: nat -> stream A) (n: nat),
  match partial_stream_clen' h n return option A with
  | Some (k, m) => h k m
  | None => None
  end = None <->
  partial_stream_clen' h n = None.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (prod nat nat) (@partial_stream_clen A h n) (@pair nat nat O n) *)
  induction n.
  + destruct (partial_stream_clen' h 0) as [[? ?] |] eqn:?H; [| tauto].
    simpl in H.
    destruct ((h 0) 0) eqn:?H; [| congruence].
    inversion H; subst.
    rewrite H0.
(* Goal: False *)
    split; intro; congruence.
  + Opaque partial_stream_clen.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
    simpl.
    Transparent partial_stream_clen.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct (partial_stream_clen h (S n)); auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h n0) n1) eqn:?H, (partial_stream_clen' h n); auto; try tauto.
(* Goal: @eq (option A) match match @stream_get A (h O) O with | Some a => @Some (prod nat nat) (@pair nat nat O O) | None => @None (prod nat nat) end with | Some (pair k m as p) => @stream_get A (h k) m | None => @None A end (@None A) *)
    rewrite H.
(* Goal: False *)
    split; intro; congruence.
Qed.

Lemma partial_stream_clen_inf0 {A: Type}: forall (h: nat -> stream A) (n: nat),
  is_inf_stream (h 0) ->
  partial_stream_clen h n = (0, n).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (prod nat nat) (@partial_stream_clen A h n) (@pair nat nat O n) *)
  induction n.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h 0) 0) eqn:?H; auto.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
(* Goal: @eq (prod nat nat) (let (k, m) := @partial_stream_clen A h n in match @stream_get A (h k) (S m) with | Some a => @pair nat nat k (S m) | None => @pair nat nat (S k) O end) (@pair nat nat O (S n)) *)
    rewrite IHn.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h 0) (S n)) eqn:?H; auto.
(* Goal: False *)
    specialize (H (S n)); congruence.
Qed.

Lemma partial_stream_clen'_inf0 {A: Type}: forall (h: nat -> stream A) (n: nat),
  is_inf_stream (h 0) ->
  partial_stream_clen' h n = Some (0, n).
Proof.
Opaque partial_stream_clen.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (prod nat nat) (@partial_stream_clen A h n) (@pair nat nat O n) *)
  induction n.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite partial_stream_clen_inf0 by auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h 0) 0) eqn:?H; auto.
(* Goal: False *)
    specialize (H 0); congruence.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite partial_stream_clen_inf0 by auto.
(* Goal: @eq (prod nat nat) (let (k, m) := @partial_stream_clen A h n in match @stream_get A (h k) (S m) with | Some a => @pair nat nat k (S m) | None => @pair nat nat (S k) O end) (@pair nat nat O (S n)) *)
    rewrite IHn.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h 0) (S n)) eqn:?H; auto.
(* Goal: False *)
    specialize (H (S n)); congruence.
Transparent partial_stream_clen.
Qed.

Lemma partial_stream_clen_fin0_left {A: Type}: forall (h: nat -> stream A) (n m: nat),
  n < m ->
  is_n_stream m (h 0) ->
  partial_stream_clen h n = (0, n).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  revert m H0 H; induction n; intros.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h 0) 0) eqn:?H; auto.
  + destruct m; [omega |].
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
    simpl.
(* Goal: @eq (prod nat nat) (let (k, m) := @partial_stream_clen A h n in match @stream_get A (h k) (S m) with | Some a => @pair nat nat k (S m) | None => @pair nat nat (S k) O end) (@pair nat nat O (S n)) *)
    rewrite (IHn (S m)) by (auto; omega).
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h 0) (S n)) eqn:?H; auto.
(* Goal: @eq (prod nat nat) (@pair nat nat (S O) O) (@pair nat nat O (S n)) *)
    pose proof (proj2 H0 (S n) H).
(* Goal: False *)
    congruence.
Qed.

Lemma partial_stream_clen'_fin0_left {A: Type}: forall (h: nat -> stream A) (n m: nat),
  n < m ->
  is_n_stream m (h 0) ->
  partial_stream_clen' h n = Some (0, n).
Proof.
Opaque partial_stream_clen.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  revert m H0 H; induction n; intros.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite (partial_stream_clen_fin0_left _ _ m) by auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h 0) 0) eqn:?H; auto.
(* Goal: False *)
    pose proof (proj2 H0 0 H); congruence.
  + destruct m; [omega |].
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
    simpl.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite (partial_stream_clen_fin0_left _ _ (S m)) by auto.
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    rewrite (IHn (S m) H0) by omega.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h 0) (S n)) eqn:?H; auto.
(* Goal: False *)
    pose proof (proj2 H0 (S n) H); congruence.
Transparent partial_stream_clen.
Qed.

Lemma partial_stream_clen'_left {A: Type}: forall (h: nat -> stream A) (n: nat),
  is_at_least_n_stream (S n) (h 0) ->
  partial_stream_clen' h n = Some (0, n).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option (prod nat nat)) (@partial_stream_clen' A h n) (@Some (prod nat nat) (@pair nat nat O n)) *)
  rewrite at_least_n_stream_spec in H.
(* Goal: @eq (option (prod nat nat)) (@partial_stream_clen' A h n) (@Some (prod nat nat) (@pair nat nat O n)) *)
  destruct H as [[m [? ?]] |].
  + eapply partial_stream_clen'_fin0_left; eauto.
  + apply partial_stream_clen'_inf0; auto.
Qed.

Lemma partial_stream_clen_fin0_right {A: Type}: forall (h: nat -> stream A) (n m: nat),
  n > 0 ->
  is_n_stream n (h 0) ->
  partial_stream_clen h (m + n) = 
  match partial_stream_clen (fun k => h (S k)) m with
  | (k1, k2) => (S k1, k2)
  end.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (prod nat nat) (@partial_stream_clen A h (Init.Nat.add m n)) (let (k1, k2) := @partial_stream_clen A (fun k : nat => h (S k)) m in @pair nat nat (S k1) k2) *)
  destruct n; [omega |].
(* Goal: @eq (prod nat nat) (@partial_stream_clen A h (Init.Nat.add m (S n))) (let (k1, k2) := @partial_stream_clen A (fun k : nat => h (S k)) m in @pair nat nat (S k1) k2) *)
  induction m.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
(* Goal: @eq (prod nat nat) (let (k, m) := @partial_stream_clen A h n in match @stream_get A (h k) (S m) with | Some a => @pair nat nat k (S m) | None => @pair nat nat (S k) O end) (@pair nat nat (S O) O) *)
    rewrite (partial_stream_clen_fin0_left _ _ (S n)) by (auto; omega).
(* Goal: @eq (prod nat nat) match @stream_get A (h O) (S n) with | Some a => @pair nat nat O (S n) | None => @pair nat nat (S O) O end (@pair nat nat (S O) O) *)
    rewrite (proj1 H0).
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    auto.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
(* Goal: @eq (prod nat nat) (let (k, m) := @partial_stream_clen A h (Init.Nat.add m (S n)) in match @stream_get A (h k) (S m) with | Some a => @pair nat nat k (S m) | None => @pair nat nat (S k) O end) (let (k1, k2) := let (k, m) := @partial_stream_clen A (fun k : nat => h (S k)) m in match @stream_get A (h (S k)) (S m) with | Some a => @pair nat nat k (S m) | None => @pair nat nat (S k) O end in @pair nat nat (S k1) k2) *)
    rewrite IHm.
(* Goal: @eq (prod nat nat) (let (k, m) := let (k1, k2) := @partial_stream_clen A (fun k : nat => h (S k)) m in @pair nat nat (S k1) k2 in match @stream_get A (h k) (S m) with | Some a => @pair nat nat k (S m) | None => @pair nat nat (S k) O end) (let (k1, k2) := let (k, m) := @partial_stream_clen A (fun k : nat => h (S k)) m in match @stream_get A (h (S k)) (S m) with | Some a => @pair nat nat k (S m) | None => @pair nat nat (S k) O end in @pair nat nat (S k1) k2) *)
    destruct (partial_stream_clen (fun k : nat => h (S k)) m).
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h (S n0)) (S n1)); auto.
Qed.

Lemma partial_stream_clen'_fin0_right {A: Type}: forall (h: nat -> stream A) (n m: nat),
  n > 0 ->
  is_n_stream n (h 0) ->
  partial_stream_clen' h (m + n) = 
  match partial_stream_clen' (fun k => h (S k)) m with
  | Some (k1, k2) => Some (S k1, k2)
  | None => None
  end.
Proof.
Opaque partial_stream_clen.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (prod nat nat) (@partial_stream_clen A h (Init.Nat.add m n)) (let (k1, k2) := @partial_stream_clen A (fun k : nat => h (S k)) m in @pair nat nat (S k1) k2) *)
  destruct n; [omega |].
(* Goal: @eq (prod nat nat) (@partial_stream_clen A h (Init.Nat.add m (S n))) (let (k1, k2) := @partial_stream_clen A (fun k : nat => h (S k)) m in @pair nat nat (S k1) k2) *)
  induction m.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
    change (partial_stream_clen h (S n)) with (partial_stream_clen h (0 + S n)).
    rewrite (partial_stream_clen_fin0_right _ _ 0) by (auto; omega).
    rewrite (partial_stream_clen'_fin0_left _ _ (S n)) by (auto; omega).
    destruct (partial_stream_clen (fun k : nat => h (S k)) 0).
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h (S n0)) n1); auto.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  + simpl.
    change (partial_stream_clen h (S (m + S n))) with (partial_stream_clen h (S m + S n)).
    rewrite (partial_stream_clen_fin0_right _ _ (S m)) by (auto; omega).
(* Goal: @eq (prod nat nat) (let (k, m) := @partial_stream_clen A h (Init.Nat.add m (S n)) in match @stream_get A (h k) (S m) with | Some a => @pair nat nat k (S m) | None => @pair nat nat (S k) O end) (let (k1, k2) := let (k, m) := @partial_stream_clen A (fun k : nat => h (S k)) m in match @stream_get A (h (S k)) (S m) with | Some a => @pair nat nat k (S m) | None => @pair nat nat (S k) O end in @pair nat nat (S k1) k2) *)
    rewrite IHm.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct (partial_stream_clen (fun k : nat => h (S k)) (S m)); auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct ((h (S n0)) n1); auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    destruct (partial_stream_clen' (fun k : nat => h (S k)) m) as [[? ?] |]; auto.
Transparent partial_stream_clen.
Qed.

Program Definition stream_capp {A: Type} (h: nat -> stream A): stream A :=
  fun n: nat =>
    match partial_stream_clen' h n return option A with
    | Some (k, m) => h k m
    | None => None
    end.
Next Obligation.
  assert (x <= y) by omega; clear H.
  rewrite partial_stream_clen'_None_iff in H0 |- *.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  induction H1; auto.
  clear H0 H1 x.
  Opaque partial_stream_clen.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  simpl.
  Transparent partial_stream_clen.
  destruct (partial_stream_clen h (S m)) as [k n].
  rewrite IHle.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  destruct (h k n); auto.
Qed.

Lemma stream_capp_spec1 {A: Type}: forall (h: nat -> stream A) (m: nat),
  is_at_least_n_stream (S m) (h 0) ->
  stream_capp h m = h 0 m.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  simpl.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  rewrite partial_stream_clen'_left by auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  auto.
Qed.

Lemma stream_capp_spec1' {A: Type}: forall (h: nat -> stream A) (m: nat) a,
  h 0 m = Some a ->
  stream_capp h m = Some a.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  rewrite stream_capp_spec1; auto.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  hnf; intros.
(* Goal: not (@eq (option A) (@stream_get A (h O) n') (@None A)) *)
  intro.
(* Goal: False *)
  rewrite (stream_sound1 (h 0) n' m) in H by (auto; omega).
(* Goal: False *)
  congruence.
Qed.

Lemma stream_capp_spec2 {A: Type}: forall (h: nat -> stream A) (n m: nat),
  n > 0 ->
  is_n_stream n (h 0) ->
  stream_capp h (m + n) = stream_capp (fun n => h (S n)) m.
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  simpl.
(* Goal: @eq (option A) match @partial_stream_clen' A h (Init.Nat.add m n) with | Some (pair k m as p) => @stream_get A (h k) m | None => @None A end match @partial_stream_clen' A (fun n : nat => h (S n)) m with | Some (pair k m as p) => @stream_get A (h (S k)) m | None => @None A end *)
  rewrite (partial_stream_clen'_fin0_right _ _ m H H0).
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  destruct (partial_stream_clen' (fun n0 : nat => h (S n0)) m) as [[? ?] |]; auto.
Qed.

Lemma stream_capp_empty0 {A: Type}: forall (h: nat -> stream A),
  is_empty_stream (h 0) ->
  is_empty_stream (stream_capp h).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @is_empty_stream A (@stream_capp A h) *)
  split; [| intros; omega].
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) O) (@None A) *)
  simpl.
(* Goal: @eq (option A) match match @stream_get A (h O) O with | Some a => @Some (prod nat nat) (@pair nat nat O O) | None => @None (prod nat nat) end with | Some (pair k m as p) => @stream_get A (h k) m | None => @None A end (@None A) *)
  destruct H as [? _].
(* Goal: @eq (option A) match match @stream_get A (h O) O with | Some a => @Some (prod nat nat) (@pair nat nat O O) | None => @None (prod nat nat) end with | Some (pair k m as p) => @stream_get A (h k) m | None => @None A end (@None A) *)
  rewrite H.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
  auto.
Qed.

Lemma stream_capp_cons {A: Type}: forall (h: nat -> stream A),
  ~ is_empty_stream (h 0) ->
  stream_capp h = stream_app (h 0) (stream_capp (fun n => h (S n))).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  stream_extensionality m.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) m) (@stream_get A (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) m) *)
  destruct (at_most_n_stream_or_at_least_Sn_stream (h 0) m).
  + rewrite at_most_n_stream_spec in H0.
(* Goal: @eq (option A) (@stream_get A (@stream_capp A h) m) (@stream_get A (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) m) *)
    destruct H0 as [n [? ?]].
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    replace m with (m - n + n) by omega.
    rewrite stream_capp_spec2;
      [| destruct (Nat.eq_dec n 0); [subst; tauto | omega] | auto].
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite stream_app_spec2 by auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    auto.
  + rewrite stream_capp_spec1 by auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite stream_app_spec1 by auto.
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    auto.
Qed.

Lemma stream_map_stream_capp {A B: Type}: forall (f: A -> B) (h: nat -> stream A),
  stream_map f (stream_capp h) = stream_capp (fun n => stream_map f (h n)).
Proof.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.
(* Goal: @eq (stream B) (@stream_map A B f (@stream_app A h1 h2)) (@stream_app B (@stream_map A B f h1) (@stream_map A B f h2)) *)
  stream_extensionality n.
(* Goal: @eq (prod nat nat) (@partial_stream_clen A h n) (@pair nat nat O n) *)
  revert h; strong_induction n.
(* Goal: forall (h : forall _ : nat, stream A) (_ : not (@is_empty_stream A (h O))), @eq (stream A) (@stream_capp A h) (@stream_app A (h O) (@stream_capp A (fun n : nat => h (S n)))) *)
  intros.

  destruct (classic (is_empty_stream (h 0))).
  Focus 1. {
    clear IH.
    pose proof proj1 (stream_map_n_stream f (h 0) 0) H.
    apply stream_capp_empty0 in H.
    apply (stream_map_n_stream f) in H.
    apply (stream_capp_empty0 (fun n : nat => stream_map f (h n))) in H0.
    destruct H as [H _], H0 as [H0 _].
    rewrite (stream_sound1 _ 0 n) by (auto; omega).
    rewrite (stream_sound1 _ 0 n) by (auto; omega).
(* Goal: @eq (option B) match @stream_get A h2 (Init.Nat.sub n m) with | Some a => @Some B (f a) | None => @None B end match @stream_get A h2 (Init.Nat.sub n m) with | Some a => @Some B (f a) | None => @None B end *)
    reflexivity.
  } Unfocus.

  destruct (at_most_n_stream_or_at_least_Sn_stream (h 0) n).
  + rewrite at_most_n_stream_spec in H0.
    destruct H0 as [m [? ?]].
(* Goal: le (Init.Nat.sub x n) (Init.Nat.sub y n) *)
    replace n with (n - m + m) by omega.
    rewrite stream_capp_spec2;
      [| destruct (Nat.eq_dec m 0); [subst; tauto | omega]
       | apply stream_map_n_stream; auto].
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    rewrite stream_capp_cons by auto.
    rewrite stream_map_stream_app.
(* Goal: @eq (option B) match @stream_get A h2 (Init.Nat.sub n m) with | Some a => @Some B (f a) | None => @None B end (@stream_get B (@stream_app B (@stream_map A B f h1) (@stream_map A B f h2)) (Init.Nat.add (Init.Nat.sub n m) m)) *)
    rewrite stream_app_spec2 by (apply stream_map_n_stream; auto).
    apply IH.
    destruct (Nat.eq_dec m 0); [| omega].
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    subst; tauto.
  + rewrite stream_capp_cons by auto.
    rewrite stream_capp_spec1 by (apply stream_map_at_least_n_stream; auto).
    rewrite stream_map_stream_app.
(* Goal: @eq (option B) (@stream_get B (@stream_map A B f (@stream_app A h1 h2)) n) (@stream_get B (@stream_app B (@stream_map A B f h1) (@stream_map A B f h2)) n) *)
    rewrite stream_app_spec1 by (apply stream_map_at_least_n_stream; auto).
(* Goal: @eq (option A) (@stream_get A (h O) m) (@stream_get A (h O) m) *)
    auto.
Qed.