proposition: Lemma iter_trans g : Transitive (iter g).
proof: Proof. move=> s2 s1 s3; case=>n; elim: n s1 =>[|n IH] s1 /=; first by move=>->. by case=>s [H1 H2] /(IH _ H2) [m]; exists m.+1, s. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)