proposition: Lemma DP_ph1_unique d1 d2 : DP_ph1 d1 -> DP_ph1 d2 -> flatten d1 = flatten d2 -> d1 = d2.
proof: Proof. move En: (size d1 + size d2) => n. have: size d1 <= n by rewrite -En ; apply leq_addr. have: size d2 <= n by rewrite -En ; apply leq_addl. have T a l: DP_ph1 (a :: l) -> ~~ nilp (flatten (a :: l)). rewrite /nilp /= size_cat; move/DP_ph1_nonempty => /= /andP[] /negbTE => ha _. by rewrite negbT // addn_eq0 -/(nilp a) ha. elim: n d1 d2 {En}. by move => d1 d2; rewrite !leqn0 => /nilP -> /nilP. move => n Hr; case. by case => // a l _ _ _;move/T => sa sb; move: sa; rewrite - sb. move => a d1; case; first by move => _ _ /T sa _ sb ; move: sa; rewrite sb. move => b d2 /=;rewrite 2!ltnS; wlog:a d1 b d2 /size a <= size b. move => hh; case /orP:(leq_total (size a) (size b)); first by apply: hh. by move => sa sb sc ha hb /esym hc; symmetry; apply:hh. move => lsab sd2n sd1n ph1 ph2 sv {T}. have bv: b = a ++ (drop (size a) b). move/eqP: sv. rewrite - {1 2} (cat_take_drop (size a) b) - catA. by rewrite eqseq_cat ?(size_takel lsab)// => /andP[/eqP <- _]. move: ph1 ph2; rewrite 2!DP_ph1_simp => /and3P[pa pb pc]/and3P[qa qb qc]. suff eab: a = b. move: sv; rewrite eab => /eqseq_cat1 ha. by rewrite (Hr _ _ sd2n sd1n pa qa ha). move: lsab;rewrite leq_eqVlt => /orP [] lsab. by rewrite bv (eqP lsab) drop_size cats0. have dd x: DP_ph1_aux2 x -> Dyck_path x. by case/orP; [move => /eqP -> | move=> /andP[_ /andP [] ]]. have lsab': (size a).+2 <= size b. move: lsab;rewrite(Dyck_size_even (dd _ pc)) (Dyck_size_even (dd _ qc)). by rewrite ltn_double -doubleS leq_double. case/orP:qc => bp1. move: lsab'; rewrite (eqP bp1) /= 2!ltnS leqn0 => ae. by case/orP: pc; [ move/eqP | rewrite /nilp ae]. move/andP:bp1 => [bp1 bp2]. case av: (a == DyckFT). by move/eqP:av => av; move:bp2;rewrite bv av (negbTE (DP_NH1_prop2 _)). have bv': flatten d1 = drop (size a) b ++ flatten d2. by move: sv; rewrite {1} bv - catA => /eqseq_cat1 . case/or3P: pb => pb. + by move: av; rewrite -(DP_ph1_size2 pc pb) eqxx. + move/nilP: pb => pb; move:(f_equal size sv) lsab. by rewrite pb /= cats0 size_cat ltnNge=> -> //; rewrite leq_addr. + move:(DP_NH1_prop1 (drop (size a).+2 b) (DP_ph1_Dyck_aux pc)). have sz1:size (a ++ DyckFT) = size (take (size a).+2 b). by rewrite size_cat addn2 (size_takel lsab'). suff: b = (a ++ DyckFT) ++ (drop (size a).+2 b) by move => <-; rewrite bp2. move/eqP: sv; move: pa pb; case: (d1) => // u v /=; rewrite DP_ph1_simp. move => /and3P [_ _ xx] /(DP_ph1_size2 xx) ->. rewrite - {1 2} (cat_take_drop (size a).+2 b) - catA (catA a). by rewrite (eqseq_cat _ _ sz1) => /andP[/eqP <- _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)