proposition: Lemma iter_pres' A (g : Rel A) n C : preserved C g -> preserved C (iter' g n).
proof: Proof. move=>coh; elim: n=>[|n IH] x y /=; first by move=><-. by case=>z [/coh H1] H2 /H1; apply: IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)