proposition: Lemma nsreachable_unique n m s : nsreachable n s -> nsreachable m s -> n = m.
proof: Proof. intros (H1, H2) (H3, H4). case (Nat.le_gt_cases n m); intros HH0. apply Nat.le_lteq in HH0; destruct HH0 as [HH0|HH0]; auto. case (H4 n); auto. - case (H2 m); auto. Qed.
imports: ZArith List