proposition: Lemma Dyck_modify_inv l: (Dyck_modify (Dyck_modify l)) = l.
proof: Proof. have H s: swap_but_last (swap_but_last s) = s. rewrite/swap_but_last revK -{2} (revK s); case: (rev s) => // a s'. by rewrite /= - map_comp /comp map_id_in // => i _; case:i. move:(Dyck_modify_split l) => /andP[/eqP ha /eqP hb]. by rewrite {1}/Dyck_modify ha hb H DP_splita_recover. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)