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