proposition: Lemma srel_step_max x : srel (size x).+2 x =2 step M x.
proof: Proof. move => c d /=. by rewrite /srel neq_ltn ltn_ord orbT andbT. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)