proposition: Lemma DP_posW l: DP_pos l -> DP_Fcount l <= DP_Tcount l.
proof: Proof. by case:l => // a l /andP[]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)