proposition: Lemma eventually_dist_cons : forall A (P:A->Prop) s x, eventually P s -> ~ P x -> dist_to_next P s < dist_to_next P (x:::s).
proof: Proof. Proof using. introv H Nx. unfold dist_to_next. epsilon n. apply~ eventually_to_dist. intros Pn. epsilon n'. apply~ eventually_to_dist. apply~ eventually_tail. intros Pn'. clearbody n n'. destruct n'; simpl in Pn'; tryfalse. rewrite* (@first_st_at_inj n n' A P s). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat