proposition: Lemma Dyck_of_Dyck_hsz D : tval D \is a Dyck_word -> Dyck_of_bal D = D.
proof: Proof. move => HD; apply val_inj => /=. suff -> : pfminh (rcons D }}) = size (rcons D }}). by rewrite rot_size -cats1 take_size_cat. apply/esym/pfminhE => //; rewrite take_size. - rewrite height_take_leq => i. rewrite leq_eqVlt => /orP[/eqP->{i} |]; first by rewrite take_size. rewrite size_rcons ltnS => Hi. rewrite -cats1 (takel_cat _ Hi) !height_simpl /=. move: HD => /Dyck_wordP[Hpos ->]. rewrite addr0 add0r. apply: (le_trans _ (Hpos _)). by rewrite -oppr_ge0 opprK. - move=> i; rewrite size_rcons ltnS => Hi. rewrite -cats1 (takel_cat _ Hi) !height_simpl /=. move: HD => /Dyck_wordP[Hpos ->]. by rewrite addr0 add0r -subr_gt0 opprK ltzD1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree