proposition: Lemma nonzero_not_infzeros: forall s (ZST: zeros_star nonzero s) (INF: infzeros s), False.
proof: Proof. intros. revert INF. induction ZST. - intro INF. punfold INF. dependent destruction INF. dependent destruction BASE. intuition. - intro INF. apply IHZST. punfold INF. dependent destruction INF. pclearbot. eauto. Qed.
imports: ZArith List String Paco.paco Program Classical