proposition: Lemma all_greater_than_m__are_here : forall n m : nat, Str_nth n (from m) = n + m.
proof: Proof. simple induction n. trivial. intros. rewrite plus_Snm_nSm. unfold Str_nth in |- *. unfold Str_nth in H. simpl in |- *. apply H. Qed.
imports: Plus Streams