proposition: Lemma infzeros_or_finzeros: forall s, infzeros s \/ zeros_star nonzero s.
proof: Proof. intros. destruct (classic (zeros_star nonzero s)); eauto. left. revert s H. pcofix CIH. intros. destruct s. - exfalso. eauto. - destruct n; [|exfalso; eauto]. pfold. econstructor. right. eauto. Qed.
imports: ZArith List String Paco.paco Program Classical