The mathematical definition of adding in a set is followed, i.e. the
element e is added only and only if it is not yet present in the set.
As this add feature is actually using is_equal, you may consider to use fast_add for expanded
objects as well while trying to get the very best performances.
e /= Void
not_in_then_added: not old has(e) implies count = old count + 1
in_then_not_added: old has(e) implies count = old count