proposition: Theorem join_Dyck_inj D1 D2 E1 E2 : [Dyck {{D1}}D2] = [Dyck {{E1}}E2] -> (D1, D2) = (E1, E2).
proof: Proof. have join_Dyck_nnil d1 d2 : [Dyck {{ d1 }} d2] != [Dyck of [::]] by []. have Dyck_fact_size (d1 d2 : Dyck) : (size d1).+2 = ex_minn (Dyck_cut_ex (join_Dyck_nnil d1 d2)). case: ex_minnP => cut /andP[Hcut /eqP Heq Hmin]. apply/anti_leq/andP; split. - move: Heq => /eqP {Hmin}; rewrite leqNgt; apply contraL; rewrite ltnS. case: cut Hcut => [// | cut _]; rewrite ltnS => Hcut. rewrite /= take_cat. move: Hcut; rewrite leq_eqVlt => /orP[/eqP -> | ->]. + rewrite ltnn subnn /= !height_simpl /= addr0. by case: d1 => /= [d1 /Dyck_wordP[_ ->]]; rewrite addr0. + rewrite !height_simpl /=. case: d1 => /= [d1 /Dyck_wordP[/(_ cut) H _]]. by apply lt0r_neq0; rewrite ltz1D. - apply: Hmin; rewrite /= {Heq}. rewrite -cat1s -[}} :: _]cat1s !catA take_size_cat ?size_cat /= ?addn1 //. rewrite !height_simpl /= addr0 addrC subrK. by case: d1 => /= [d1 /Dyck_wordP[_ ->]]. move=> Heq. have Hnnil := join_Dyck_nnil D1 D2. move: (Dyck_fact_size D1 D2). rewrite (eq_ex_minn _ (Dyck_cut_ex (join_Dyck_nnil E1 E2))); last by move=> i; rewrite Heq. rewrite -(Dyck_fact_size E1 E2) => /eqP; rewrite !eqSS => /eqP Hsz. move: Heq => /(congr1 val)/= /eqP. rewrite -[{{ :: _ ++ _]cat1s -[}} :: D2]cat1s !catA. rewrite -[{{ :: _ ++ _]cat1s -[}} :: E2]cat1s !catA. rewrite !eqseq_cat /= ?size_cat ?Hsz //=. by move=> /andP[/andP[/eqP /val_inj -> _] /eqP /val_inj ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree