proposition: Lemma DP_NH1_prop1 x y: Dyck_path y -> ~~ Dyck_NH1 ((y ++ DyckFT) ++ x).
proof: Proof. move => dpy; apply/negP => /andP [bp2]. have dp1: Dyck_path(y ++ DyckFT) by apply: Dyck_path_cat. have hh: Dyck_irred DyckFT by []. rewrite /DP_NH1(DP_splitc_cat dp1 (Dyck_sub_path dp1 bp2)). by rewrite (DP_splitc_cat dpy) // 2!all_cat (DP_splitc_irred hh) /= andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)