proposition: Lemma DP_count_sym l1 l2: DP_balanced (l1 ++ l2) -> (DP_Fcount l2 <= DP_Tcount l2) = (DP_Tcount l1 <= DP_Fcount l1).
proof: Proof. move/eqP; rewrite /DP_Fcount /DP_Tcount !count_cat. case:(leqP ((count_mem true) l1) ((count_mem false) l1)) => sa; case:(leqP ((count_mem false) l2) ((count_mem true) l2)) => sb // eq1. by move: (leq_add sa sb); rewrite addnS eq1 ltnn. by move: (leq_add sa sb); rewrite addSn eq1 ltnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)