proposition: Lemma next_not_acc : forall a, ~ Acc R a -> exists b, R b a /\ ~ Acc R b.
proof: Proof. intros a H1; apply not_all_not_ex. intros H2; apply H1. split; intros y H3. specialize (H2 y); apply not_and_or in H2. destruct H2;auto. - contradiction. - now apply NNPP in H2. Qed.
imports: Relations Classical ClassicalChoice