proposition: Lemma Dyck_lp_size n l: Dyck_path l -> size l = n.+1.*2 -> size (Dyck_lp l) = n.*2.
proof: Proof. move => h. rewrite -{1}(DP_splitc_recover l). rewrite /Dyck_lp size_drop !size_flatten. set A := shape _; set B := shape _; suff: A = B by move => -> ->; rewrite subn2. rewrite /A/B; move:(DP_splitc_correct h);elim: (DP_splitc l) => // a s Hr. move => /= /andP [/andP[/eqP {2} -> _] /Hr <-]. by rewrite /DP_raise /= size_rcons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)