proposition: Lemma srelLR k x p i q j : srel k x (p,i) (q,j) -> j.+1 = i :> nat \/ j = i.+1 :> nat.
proof: Proof. case/srel_step/orP => /andP [_ /eqP ->]; tauto. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)