proposition: Lemma set_iterF_mono : {homo iterF : i j / i <= j >-> i \subset j}.
proof: Proof. by apply: homo_leq => //[???|]; [apply: subset_trans|apply: set_iterF_sub]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)