proposition: Lemma principal_filter_ultra {T : Type} (x : T) : UltraFilter (principal_filter x).
proof: Proof. split=> [|G [G0 xG] FG]; first exact: principal_filter_proper. rewrite eqEsubset; split => // U GU; apply/principal_filterP. have /(filterI GU): G [set x] by exact/FG/principal_filterP. by rewrite setIC set1I; case: ifPn => // /[!inE]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed