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