proposition: Lemma iters_aux_nreach n m ps : (forall s, In s (fst ps) <-> nlreachable m s) /\ (forall s, (nsreachable m s -> In s (snd ps)) /\ (In s (snd ps) -> nlreachable m s)) -> (forall s, In s (fst (iters_aux n ps)) <-> nlreachable (n + m) s) /\ (forall s, (nsreachable (n + m) s -> In s (snd (iters_aux n ps))) /\ (In s (snd (iters_aux n ps)) -> nlreachable (n + m) s)).
proof: Proof. revert m ps; elim n; simpl; auto; clear n. intros n Hrec m (ss1, ss2); simpl fst; simpl snd. replace (S (n + m)) with (n + (S m)); auto with arith. intros H1; apply Hrec. apply (fold_nexts_nreach m (ss1, ss2)); auto. Qed.
imports: ZArith List