proposition: Lemma openE_subproof : op = [set A : set T | A `<=` nbhs^~ A].
proof: Proof. rewrite predeqE => A; split=> [Aop p Ap|Aop]. by exists A; split=> //; split. suff -> : A = \bigcup_(B : {B : set T & op B /\ B `<=` A}) projT1 B. by apply: op_bigU => B; have [] := projT2 B. rewrite predeqE => p; split=> [|[B _ Bp]]; last by have [_] := projT2 B; apply. by move=> /Aop [B [Bop Bp sBA]]; exists (existT _ B (conj Bop sBA)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed