fact: Fixpoint lazy_seq {A : Type} (s : A -> A) (lo : A) (len : nat) := match len with | O => lnil | S len' => lcons lo (fun tt => lazy_seq s (s lo) len') end.
imports: ExtLib.Structures(Functor Applicative) List QuickChick(Tactics) Coq(ssreflect)