proposition: Lemma count_rcons w P l : count P (rcons w l) = count P w + P l.
proof: Proof. Proof using. by rewrite -count_rev rev_rcons /= count_rev addnC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)