proposition: Lemma Dyck_rp_size l: Dyck_path l -> size (Dyck_rp l) = (size l).+2.
proof: Proof. move => dp. move:(Dyck_rp_prop dp) => /and4P[ha /eqP hb _ _]. move/(f_equal size): hb; rewrite[size (prependFT l)] /= => <-. rewrite 2!size_flatten /shape -map_comp /comp; congr sumn; apply/ eq_in_map. by move => t /(allP ha)/andP[tu _]; apply:Dyck_rp_aux_size. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)