proposition: Lemma size_del (T: eqType) (x:T) s : x \in s -> size (del x s) < size s.
proof: Proof. move => in_s. rewrite size_filter -(count_predC [pred a | a != x]). rewrite -{1}[count _ s]addn0 ltn_add2l -has_count. apply/hasP. exists x => //. by rewrite inE /= eqxx. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)