proposition: Lemma fsets_self (F : set T) : finite_set F -> fsets F F.
proof: Proof. by move=> finF; split. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun