proposition: Lemma notSN_succ : exists y, R x y /\ ~SN R y.
proof: Proof. cut (~(forall y, R x y -> SN R y)). intro. ded (not_forall_imply_exists_not H). destruct H0. ded (imply_to_and _ _ H0). exists x0. auto. eapply contraposee_inv. apply SN_intro. exact h. Qed.
imports: Coq(Relations) CoLoR(ClassicUtil SN LogicUtil)