proposition: Lemma move_nsreachable n s2 : nsreachable (S n) s2 -> exists s1, move s1 s2 /\ nsreachable n s1.
proof: Proof. intros (H1, H2). case (move_nreachable _ _ H1); intros s1 (Hs1, Hs2). exists s1; split; auto. case (nsreachable_bound _ _ Hs2); intros m (Hm, Hm1). apply Nat.le_lteq in Hm; destruct Hm as [Hm|Hm]. - case (H2 (S m)); auto with arith. apply nreachS with (2 := Hs1); auto. case Hm1; auto. - subst n; auto. Qed.
imports: ZArith List