proposition: Lemma count_memE x (t : syntax) : count_mem x t = pos 0%num (content t) x.
proof: Proof. rewrite /content; set loop := (X in X Empty); rewrite -/loop. rewrite -[LHS]addn0; have <- : pos 0%num Empty x = 0 :> nat by elim: x. elim: t Empty => [n|s IHs s' IHs'] e //=; last first. by rewrite serial_Op count_cat -addnA IHs' IHs. rewrite ?addn0 set_pos_trecE pos_set_pos; case: (altP eqP) => [->|] //=. by rewrite -N.add_1_l nat_of_add_bin //=. Qed.
imports: HB(structures) BinPos BinNat mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq bigop)