proposition: Lemma iter_pres A (g : Rel A) C : preserved C g -> preserved C (iter g).
proof: Proof. by move=>pres x y [n] /(iter_pres' pres). Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)