proposition: Lemma iter'_sub g g' n s1 s2 : (forall s1 s2, g s1 s2 -> g' s1 s2) -> iter' g n s1 s2 -> iter' g' n s1 s2.
proof: Proof. by move=>H; elim: n s1=>[|n IH] s1 //= [s][/H G] /IH; exists s. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)