proposition: Lemma srel1 k x c d : srel k x c d -> d.2 <= c.2.+1.
proof: Proof. move: c d => [p i] [q j] /srelLR [<-|->] //=. by ssrlia. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)