proposition: Lemma Dyck_modify_split l (s := (Dyck_modify l)) : ((DP_splita s).1 == swap_but_last (DP_splita l).1) && ((DP_splita s).2 == (DP_splita l).2).
proof: Proof. have H v: nilp ((DP_splita v).1) -> (DP_splita v).2 = v. by move/nilP=> ea; move: (DP_splita_recover v); rewrite ea. rewrite /s /Dyck_modify. case/orP:(DP_splita_correct l) => /= [ok | /andP [ha hb] ]. by move/nilP: (ok) => eq1; rewrite (H _ ok) eq1 /= eq1 (H _ ok) ! eqxx. set l1 := (DP_splita l).1. have hc: ends_withF (swap_but_last l1). move: ha; rewrite /ends_withF -/l1 -{1} (revK l1) /swap_but_last. by case: (rev l1) => // a l'; rewrite /=!rev_cons !last_rcons /=. set l3:=(swap_but_last l1). have ->:l3 = rcons (rev (behead (rev l3))) false. move /eqP: hc; rewrite -/l3 -{1 2} (revK l3); case: (rev l3) => //. by move => a l';rewrite rev_cons last_rcons /= => ->. elim: (rev _). move/andP:hb => [/eqP h]; rewrite DP_splita_pos1 =>h1. by rewrite /= h1 add1n add0n h ltnn !eqxx. move => a l' /andP[/eqP ha' /eqP hb']; rewrite rcons_cons cat_cons /= ha' hb'. by rewrite /nilp size_rcons /= !eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)