proposition: Lemma iters_aux_valid n ps : valid_pair ps -> valid_pair (iters_aux n ps).
proof: Proof. revert ps; elim n; simpl; auto; clear n. intros n Hrec (sl, sr) Hg. apply Hrec; apply (fold_nexts_valid (sl, sr)); auto. intros s1 HH; case HH. Qed.
imports: ZArith List