proposition: Lemma reachable_nreachable s : reachable s -> exists n, nreachable n s.
proof: Proof. intros H; elim H; clear s H; try (exists 0%nat; apply nreach0); intros s Hs (n, Hrec); exists (S n); apply nreachS with s; auto; unfold move; auto; do 6 right; auto. Qed.
imports: ZArith List