Library prosa.classic.util.seqset

Require Export prosa.util.seqset.

From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq fintype.

Section Lemmas.

  Context {T: eqType}.
  Variable s: {set T}.

  Lemma set_mem : ∀ x, (x \in s) = (x \in _set_seq s).

End Lemmas.

Section LemmasFinType.

  Context {T: finType}.
  Variable s: {set T}.

  Lemma set_card : #|s| = size s.

End LemmasFinType.