proposition: Lemma LimitNotSucc (alpha: A) : Limit alpha -> forall beta, ~ Successor alpha beta.
proof: Proof. intros [[w H] H0] beta [H1 H2]. destruct (lt_eq_lt beta w) as [H3 | [H3 | H3]]. - apply (H2 w);auto. - subst w; destruct (H0 _ H1) as [z [H3 H4]]; apply (H2 z);auto. - destruct (H0 beta H1) as [z [H4 H5]]; eauto. Qed.
imports: Coq(Relations RelationClasses Setoid)