proposition: Lemma iterS g n s1 s2 : iter' g n.+1 s1 s2 <-> exists s, iter' g n s1 s /\ g s s2.
proof: Proof. elim: n s1=>[|n IH] s1. - by split; [case=>s [H <-]; exists s1 | case=>s [<- H]; exists s2]. split; first by case=>s [H1] /IH [s'][H G]; exists s'; split=>//; exists s. by case=>s [[s'][H1 H G]]; exists s'; split=>//; apply/IH; exists s. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)