proposition: Theorem factor_Dyck D : D != [Dyck of [::]] -> { DD : Dyck * Dyck | D = [Dyck {{ DD.1 }} DD.2] }.
proof: Proof. move=> Hnnil. case: (ex_minnP (Dyck_cut_ex Hnnil)) => cut /andP[Hcut /eqP Heq Hmin]. case: D Hnnil Heq Hmin => [[|w0 tl]] // HD _; rewrite [dyckword _]/=. case: w0 HD => HD; first last. have:= HD; rewrite unfold_in => /andP[/Dyck_prefixP/(_ 1%N)]. by rewrite /= take0 !height_simpl /= addr0. have:= (Dyck_wordP _ HD) => [[Hpos /eqP Hbal]]. case: cut Hcut => // [][|cut] _; rewrite [X in X -> _]/= !height_simpl [X in X -> _]/= ?take0 ?height_simpl //. move=> Heq Hmin. have Hcut : (cut < size tl)%N. rewrite -ltnS; apply Hmin. by rewrite -[(size tl).+1]/(size ( {{ :: tl)) take_size Hbal /=. have Hf1 : take cut.+1 tl = rcons (take cut tl) }}. move: Heq (Hpos cut.+1). rewrite /= (take_nth {{ Hcut) !height_simpl /=. case: (nth {{ tl cut) => //=. by rewrite addrC -addrA => /eqP; rewrite addr_eq0 => /eqP ->. move: Heq; rewrite Hf1 !height_simpl! /= addrC subrK => Hbalcut. have {}Hmin n : (n <= cut)%N -> height (take n tl) >= 0. apply contraLR; rewrite -ltnNge -ltNge. case: cut Hbalcut Hmin {Hcut Hf1} => [ _ _ | cut Hbalcut Hmin Hlt]. by case: n; first by rewrite take0. apply: (Hmin (n.+1)); rewrite /= height_simpl /= eq_le. apply/andP; split; first by rewrite lez1D. by have:= Hpos (n.+1); rewrite /= !height_simpl /=. have HDL : (take cut tl) \is a Dyck_word. apply/Dyck_wordP; split; last by rewrite Hbalcut. rewrite height_take_leq => n. rewrite size_take Hcut => Hncut. by rewrite take_takel // Hmin. have HDR : (drop cut.+1 tl) \is a Dyck_word. apply/Dyck_wordP; split => [n|]. - rewrite take_drop height_drop. rewrite take_takel ?ltnS ?leq_addl //. rewrite Hf1 height_rcons /= Hbalcut sub0r /=. have := Hpos ((n + cut.+1).+1)%N. by rewrite /= height_simpl /= addrC. - move: Hbal; rewrite -{1}(cat_take_drop cut.+1 tl) => /eqP. by rewrite Hf1 /= !height_simpl /= Hbalcut add0r addrA subrr add0r. exists (DyckWord HDL, DyckWord HDR). by apply/val_inj; rewrite /= -{1}(cat_take_drop cut.+1 tl) Hf1 cat_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree