proposition: Lemma DP_splitc_correct l: Dyck_path l -> all Dyck_irred (DP_splitc l).
proof: Proof. elim /size_ind:l => l Hr dl. rewrite (DP_splitc_rec l);case nn: (nilp l) => //. rewrite (negbTE(DP_splitb_prop1 dl (negbT nn))) /= all_rcons. move /andP: (DP_splitb_Dyck12 dl) => [ha _]. rewrite (DP_splitb_prop3 dl (negbT nn)) /= Hr //. exact: (DP_splitb_size_rec (negbTE (DP_splitb_prop1 dl (negbT nn)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)