proposition: Lemma Dyck_rpK l: Dyck_path l -> Dyck_lp (Dyck_rp l) = l.
proof: Proof. move => dl;rewrite /Dyck_rp/Dyck_lp. move: (Dyck_rp_prop dl) => /and4P [ha hb hc hd]. by rewrite (eqP hc) (eqP hd) (eqP hb) /= drop0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)