proposition: Lemma iter'_split g n1 n2 s1 s2 : iter' g (n1 + n2) s1 s2 -> exists s, iter' g n1 s1 s /\ iter' g n2 s s2.
proof: Proof. elim: n1 s1 s2=>[|n1 IH] s1 s2 /=; first by rewrite add0n; exists s1. by case=>s [H1] {}/IH [s'][H2 H3]; exists s'; split=>//; exists s. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)