Finset and finmap

Finset and finmap are MathComp libraries defining finite sets of finite types and finite sets of choice types, respectively. Thus, it is not possible to create a finset-set of nat, but it is possible to create a finmap-set of nat, and it is possible to create both a finset-set and a finmap-set of bool.

These libraries are similar in several ways, and knowing one brings you almost all the way to knowing the other. The main difference in notations is that finset notations use ":" to refer to set operations (eg "A :|: B" for union), while finmap uses "`" (eg "A `|` B"). The main difference in naming conventions is that finset uses "set" where finmap uses "fset". Make sure to at least skim the headers of each file before using it, and take particular note of the naming conventions described at the end of the finset header.

Some notes for finset:

1. Some notions such as \subset are defined in fintype, which is a dependency of finset.
2. Proving that two sets are equal is best accomplished through setP (this translates equality to x \in A <-> x \in B), unless there happens to already be a collection of lemmas that let you reach your goal through direct rewriting.
3. Proving A \subset B is best accomplished through subsetP, and similarly, a hypothesis that A \subset B will probably be more useful under the subsetP view.
4. Proving or manipulating statements of the form [set _ | _] is best accomplished through imsetP.
5. inE is useful to simplify expressions of the form x \in X, where X includes simplifyable set operations such as intersections, unions, etc. There are also views such as setUP that can be used in more or less the same contexts. Note that their names are easily guessable. Eg, setUP is about union.
6. Facts about operations with singletons, for example about x |: X, can be found by searching for the operation about generic sets, _ :|: _ in this case. This is because _ |: _ is just a notation for [set _] :|: _ and often there are not specific lemmas for singletons (since their proofs would be the same as for their more generic counterparts).

Finmap equivalents:

1. The notation for subset is now "`<=`" instead of "\subset"
2. Use fsetP
3. Use fsubsetP
4. Use imfsetP
5. Continue using inE. The views are named fsetUP, etc.
6. Same idea. Here notations for singletons are, eg, _ |` _, which can be found by searching _ `|` _.