proposition: Lemma iter2s_aux_valid n p ps : valid_triple ps -> valid_triple (iter2s_aux n p ps).
proof: Proof. revert p ps; elim n; simpl; auto; clear n. intros n Hrec p (sl, sr) Hg. apply Hrec; apply (fold_next2s_valid p (sl, sr)); auto. intros s1 HH; case HH. Qed.
imports: ZArith List