前回、iterateとtakeを定義した。 Require Import List. Require Import Coq.Lists.Streams. Section MyStreams. Variable A : Type. CoFixpoint iterate (f : A -> A) (x : A) : Stream A := Cons x (iterate f (f x)). Fixpoint take (n : nat) (s : Strea…