proposition: Lemma Dyck_modify_tcount_bis l (s:= (Dyck_modify l)) : DP_Fcount l = (DP_Tcount l).+2 -> ((DP_Tcount s == (DP_Tcount l).+1) && (DP_balanced s)).
proof: Proof. move => ha. suff hd: (DP_Tcount s == (DP_Tcount l).+1). rewrite hd /= /DP_balanced (eqP hd) eq_sym. rewrite - (DP_count' (m:=(DP_Tcount l).+1)) //. by rewrite (Dyck_modify_size l) - DP_count ha addSnnS. have hb: DP_pos l = false. by move: ha; clear; case: l => // a l /= ->; rewrite ltnNge leqnSn andbF. rewrite - eqSS - ha. move:(DP_splita_correct l). rewrite /= - DP_splita_pos1 hb /= => /andP[hc /andP[/eqP hd _]]. rewrite -(DP_splita_recover l) /s /Dyck_modify /DP_Tcount /DP_Fcount. by rewrite !count_cat -addSn (swap_but_last_count hc) -/(DP_Tcount _) hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)