proposition: Lemma nlreachable_bound n s : nlreachable n s -> exists m, m <= n /\ nsreachable m s.
proof: Proof. intros (m, (H1, H2)); case (nsreachable_bound m s); auto. intros p (Hp, Hp1); exists p; split; auto. apply Nat.le_trans with (1 := Hp); auto. Qed.
imports: ZArith List