proposition: Lemma swap_but_last_count l: ends_withF l -> (DP_Tcount(swap_but_last l)).+1 = DP_Fcount l.
proof: Proof. rewrite /swap_but_last - {1 3} (revK l); case: (rev l) => // a s. rewrite {1}rev_cons /ends_withF last_rcons => /eqP ->. rewrite /DP_Tcount /DP_Fcount !count_rev /= add0n add1n; congr (_.+1). by elim:s => // b s /= ->; case:b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)