proposition: Lemma nbhs_pfilter_subproof (p : T) : ProperFilter (nbhs p).
proof: Proof. apply: Build_ProperFilter. by move=> A [B [_ Bp sBA]]; exists p; apply: sBA. split; first by exists setT; split=> [|//|//]; exact: opT. move=> A B [C [Cop Cp sCA]] [D [Dop Dp sDB]]. exists (C `&` D); split=> //; first exact: opI. by move=> q [/sCA Aq /sDB Bq]. move=> A B sAB [C [Cop p_C sCA]]. by exists C; split=> //; apply: subset_trans sAB. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed