proposition: Theorem no_infinite_sequence2 : forall x : T , SN R x -> ~(exists f : nat -> T , f 0 = x /\ forall i : nat , f i -R> f (i+1)) .
proof: Proof. intros. induction H. intuition. elim H1. intros. apply (H0 (x0 1)). intuition. subst. apply (H4 0). exists ( fun i => (x0 (i+1))). intuition. Qed.
imports: Coq(Lia Relations Wellfounded) CoLoR(term)