proposition: Lemma DP_count_catTF v: DP_balanced (DP_raise v) = DP_balanced v.
proof: Proof. rewrite /DP_raise /DP_balanced/DP_Tcount/DP_Fcount /= - cats1 !count_cat /=. by rewrite !add0n !add1n addn0 addn1 eqSS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)