proposition: Lemma filterI_iter_sub {T : Type} (F : set (set T)) : {homo filterI_iter F : i j / (i <= j)%N >-> i `<=` j}.
proof: Proof. move=> + j; elim: j; first by move=> i; rewrite leqn0 => /eqP ->. move=> j IH i; rewrite leq_eqVlt => /predU1P[->//|]. by move=> /IH/subset_trans; apply=> A ?; do 2 exists A => //; rewrite setIid. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed