proposition: Lemma porder_move s1 s2 n1 n2 : nsreachable n1 s1 -> nsreachable n2 s2 -> move s1 s2 -> n1 = n2 \/ n1 = S n2 \/ S n1 = n2.
proof: Proof. intros H1 H2 H3. assert (F1: nreachable (S n2) s1). apply nreachS with s2; auto. + case H2; auto. + apply move_sym; auto. apply nreachable_valid with n1; case H1; auto. + case (nsreachable_bound _ _ F1); intros k (Hk, Hk1). assert (k = n1); subst. apply nsreachable_unique with s1; auto. assert (F2: nreachable (S n1) s2). apply nreachS with s1; auto. case H1; auto. case (nsreachable_bound _ _ F2); intros k1 (Hk2, Hk3). assert (k1 = n2); subst. apply nsreachable_unique with s2; auto. apply Nat.le_lteq in Hk; destruct Hk as [Hk|Hk]; subst; auto. apply Nat.le_lteq in Hk2; destruct Hk2 as [Hk2|Hk2]; subst; auto. left; apply le_antisym; auto with arith. Qed.
imports: ZArith List