proposition: Lemma DP_count' m n l: size l = m + n -> (DP_Tcount l == m) = (DP_Fcount l == n).
proof: Proof. move/eqP;rewrite - DP_count. case ha: (DP_Tcount l == m);first by rewrite - (eqP ha) eqn_add2l. by case hb: (DP_Fcount l == n) => //; rewrite - (eqP hb) eqn_add2r ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)