proposition: Lemma Dyck_rp_H2 l: Dyck_path l -> Dyck_NH2 (Dyck_rp l).
proof: Proof. move => dl. rewrite /Dyck_NH2/DP_NH2 (Dyck_rp_Dyck dl) /=. move:(Dyck_rp_prop dl) => /and4P; rewrite /Dyck_rp. set u:=Dyck_rp_aux2 l; set v := [seq Dyck_rp_aux s | s <- u]. move => [ha hb hc hd]; rewrite (eqP hc). apply/allP => x /mapP [y /(allP ha) /andP[pa /andP[pb pc]] ->]. by move:pc; rewrite - {1} (Dyck_rp_auxK pa) /Dyck_lp_aux /= drop0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)