proposition: Lemma all_count s : all s = (count s == size s).
proof: Proof. elim: s => //= x s; case: (a x) => _ //=. by rewrite add0n eqn_leq andbC ltnNge count_size. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)