proposition: Theorem rot_is_Dyck : take (size w).-1 (rot pfminh w) \is a Dyck_word.
proof: Proof. apply/Dyck_wordP; rewrite height_take_leq; split => [n|]. - have -> : size (take (size w).-1 (rot pfminh w)) = (size w).-1. rewrite size_take size_rot /=. by case: w Hbal1 => //= w0 tlw _; rewrite ltnSn. move => Hn; rewrite take_takel // /rot take_cat size_drop. case: ltnP => [{}Hn| Hnpf]. + rewrite take_drop height_drop take_takel ?leq_addl // subr_ge0. by rewrite pfminhP minhP. + have {Hnpf} : (n - (size w - pfminh) < pfminh)%N. rewrite subnBA ?pfminh_size // addnC -subnBA ?leq_subr; first last. exact: (leq_trans Hn (leq_pred _)). case: w Hbal1 Hn Hnpf => // w0 wtl _ /= Hn. case: pfminh pfminh_pos => // pfm _; rewrite subSS => Hsz. rewrite [(_ - n)%N]subSn // subSS ltnS. exact: leq_subr. move: (n - (size w - pfminh))%N => {}n {}Hn. rewrite height_simpl take_takel; last exact: ltnW. move: Hbal1; rewrite -{1}(cat_take_drop pfminh w) height_simpl => /eqP. rewrite -subr_eq0 opprK [height _ + _]addrC -addrA addr_eq0 => /eqP ->. rewrite addrC subr_ge0 lezD1. by rewrite pfminhP pfminh_min. - have : height (rot pfminh w) = -1. by rewrite /rot height_cat addrC -height_cat cat_take_drop. rewrite -{1}rot_pfminhE height_simpl /= => /eqP. by rewrite subr_eq => /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree