proposition: Lemma DP_split_resize_correct2 l: all Dyck_irred l -> DP_ph1 (DP_split_resize l).
proof: Proof. have H a: Dyck_irred a -> DP_ph1_aux2 a. move => h; rewrite /DP_ph1_aux2/Dyck_NH1/DP_NH1. rewrite (DP_splitc_irred h) /= (Dyck_irred_Dyck h). move/andP:h => [/eqP -> _]; rewrite size_DP_raise. by case:(DP_lower a) => // u s /=; rewrite orbT. rewrite /DP_ph1 => ha;rewrite DP_split_resize_correct1 /=. elim: l ha => // a l Hr /= /andP[/H ha /Hr hb]. case sz: (size a == 2). by rewrite /= ha hb. move: hb. case: (DP_split_resize l). by rewrite /= ha . move=> b s /= /andP[hu hv]. case sb:(size b == 2). simpl. rewrite ha hu hv //. simpl; rewrite hv andbT /DP_ph1_aux2. case/orP: ha => ha; first by move:sz; rewrite (eqP ha). case/orP: hu => hb; first by move:sb; rewrite (eqP hb). move/andP: ha => [ha1 /andP[ha2 ha3]]; move/andP: hb => [hb1 /andP[hb2 hb3]]. have ->: ~~ nilp (a ++ b). by rewrite /nilp size_cat addn_eq0 -/(nilp a)(negbTE ha1). apply/orP; right; simpl;apply/andP; split; first exact:(Dyck_path_cat ha2 hb2). by rewrite /DP_NH1 (DP_splitc_cat ha2 hb2) all_cat; apply/andP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)