proposition: Lemma nsreachable_inv n m s : n <= m -> nsreachable m s -> exists s1, nsreachable n s1.
proof: Proof. intro H; revert s; elim H; auto; clear m H. - intros s H1; exists s; auto. - intros m _ H1 s H2. case (move_nsreachable _ _ H2); intros s1 (_, Hs1); auto. apply (H1 s1); auto. Qed.
imports: ZArith List