proposition: Lemma Dyck_rp_aux_size x: starts_withFT x -> size (Dyck_rp_aux x) = size x.
proof: Proof. by rewrite starts_withFT_prop /Dyck_rp_aux /= size_rcons => /eqP{2} ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)