proposition: Lemma DP_pos_cat l1 l2: DP_pos l1 -> DP_pos l2 -> DP_pos (l1 ++ l2).
proof: Proof. move => sa sb; elim: l1 sa => // a l H /andP [ha]. rewrite /= (H ha) /= /DP_Fcount /DP_Tcount !count_cat !addnA => sa. exact: (leq_add sa (DP_posW sb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)