proposition: Lemma iter_in f S i : {homo f : x / x \in S} -> {homo iter i f : x / x \in S}.
proof: Proof. by move=> f_in x xS; elim: i => [|i /f_in]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring