proposition: Lemma gauge_filter : Filter gauge.
proof: Proof. apply: filter_from_filter; first by exists 0%N. move=> i j _ _; wlog ilej : i j / (i <= j)%N. by move=> WH; have [|/ltnW] := leqP i j; [|rewrite (setIC (iter _ _ _))]; exact: WH. exists j => //; rewrite subsetI; split => //; elim: j i ilej => [i|j IH i]. by rewrite leqn0 => /eqP ->. rewrite leq_eqVlt => /predU1P[<-//|/ltnSE/IH]; apply: subset_trans. by move=> x/= [jx _]; apply: split_ent_subset => //; exact: iter_split_ent. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed