proposition: Lemma porder_move_down s1 s2 n1 n2 : nsreachable n1 s1 -> nsreachable n2 s2 -> move s1 s2 -> porder n2 = pos_down (porder n1) -> n1 = S n2.
proof: Proof. intros H1 H2 H3; generalize (porder_move _ _ _ _ H1 H2 H3); intros [HH | [HH | HH]]; auto. - intros HH1; contradict HH1; generalize (porder_inv n1); intros [HH2 | [HH2 | HH2]]; subst; rewrite HH2; intros HH3; discriminate. - intros HH1; contradict HH1; subst; rewrite porderS; generalize (porder_inv n1); intros [HH2 | [HH2 | HH2]]; rewrite HH2; intros HH3; discriminate. Qed.
imports: ZArith List