proposition: Lemma Dyck_irrred_prop1 l1 l2: Dyck_path l1 -> Dyck_path l2 -> Dyck_irred (l1++l2) -> (nilp l1 ) || (nilp l2).
proof: Proof. move => sa sb /andP[sc sd]. case nl: (nilp l2); rewrite ?orbT ?orbF //. have dd: Dyck_path [::] by []. move: (DP_splitb_prop4 dd sd)=>/and3P[_ _]; rewrite cat0s - (eqP sc). move: (DP_splitb_race1 l1 sb (negbT nl)) => ->. rewrite -{2} (DP_splitb_recover l2) catA - {1}(cat0s (DP_splitb l2).2). rewrite eqseq_catr; case l1 => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)