Embryonic doc.

Lebesgue/Subset_seq.v

@@ -14,7 +14,14 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-(* All or parts of this file could use results on BigOps from MathComp. *)
+(** Countable iterations of operators on subsets (definitions and properties).
+
+  Subsets of type U are represented by functions of type U -> Prop.
+
+  Most identities can be found on Wikipedia:
+  https://en.wikipedia.org/wiki/List_of_set_identities_and_relations
+
+  All or parts of this file could use results on BigOps from MathComp. *)
 
 From Coq Require Import Classical FunctionalExtensionality FinFun.
 From Coq Require Import Arith Lia.