proposition: Lemma seq_infzeros_or_finzeros: forall s t (R: seq s t), (infzeros s /\ infzeros t) \/ (zeros_star nonzero s /\ zeros_star nonzero t).
proof: Proof. intros. destruct (@infzeros_or_finzeros s). - eauto using seq_infzeros_imply. - eauto using seq_zeros_star_imply. Qed.
imports: ZArith List String Paco.paco Program Classical