proposition: Lemma srel_mid (k k' : nat) x (i j : pos x) (p q : M) : i <= k <= j -> k <= k' -> reflect (exists2 p', connect (srel k x) (p,i) (p',inord k) & connect (srel k' x) (p',inord k) (q,j)) (connect (srel k' x) (p,i) (q,j)).
proof: Proof. move => H X. apply: (iffP idP). - case/connectP => cs c1 c2. case: (srel_mid_path H c1 c2) => [p'] [cl] [cr] [Ecs L C]. subst cs. rewrite cat_path last_cat -L in c1 c2. case/andP : c1 => ? c1. exists p'. + apply/connectP. by exists cl. + apply/connectP. by exists cr. - case/andP: H => H1 H2 [p']. move/(srelS (k'-k) H1). rewrite subnKC //. exact: connect_trans. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)