proposition: Lemma fsets0 : fsets set0 = [set set0].
proof: Proof. rewrite predeqE => A; split => [|->]; last exact: fsets_set0. by rewrite /fsets/= subset0 => -[]. 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