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