proposition: Lemma nsreachable_bound n s : nreachable n s -> exists m, m <= n /\ nsreachable m s.
proof: Proof. revert s; pattern n; apply Wf_nat.lt_wf_ind; clear n. intros n; case n; clear n. - intros _ s H; exists 0; split; auto with arith. split; auto; intros m Hm; contradict Hm; auto with arith. - intros n Hrec s Hs. case (nreachable_le_dec (S n) s). + apply nreachable_valid with (1 := Hs). + intros H1; exists (S n); split; auto; split; auto. + intros (m, (Hm1, Hm2)). case (Hrec _ Hm1 _ Hm2); intros s1 (Hs1, Hs2). exists s1; split; auto with arith. apply Nat.le_trans with (1 := Hs1); auto with arith. Qed.
imports: ZArith List