proposition: Lemma srel_mid_path (k k' : nat) x (i j : pos x) (p q : M) cs : i <= k <= j -> path (srel k' x) (p,i) cs -> (q,j) = last (p,i) cs -> exists p' cl cr, [/\ cs = cl ++ cr, (p',inord k) = last (p,i) cl & path (srel k x) (p,i) cl].
proof: Proof. move: cs p i. apply: (size_induction (measure := size)) => cs IH p i /andP [H1 H2]. case: (boolP (i == k :> nat)) => Ei. - exists p, [::], cs. by rewrite -[i]inord_val (eqP Ei). - destruct cs as [|c cs] => [_ /= [_ E]|/= /andP [s p1] p2]; subst. + by rewrite eqn_leq H1 H2 in Ei. + have Hi: i < k by rewrite ltn_neqAle Ei H1. have mid: c.2 <= k <= j by rewrite (leq_trans (srel1 s)). case: (IH cs _ c.1 _ mid) ; rewrite -?surjective_pairing //. move => p' [cl] [cr] [C1 C2 C3]. exists p', (c::cl), cr. rewrite /= -C1 C3 andbT. split => //. rewrite /srel /= eq_sym Ei andbT. exact: srel_step s. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)