proposition: Theorem not_decreasing (A:Type)(R: relation A) (Hwf : well_founded R) : ~ (exists seq : nat -> A, (forall i:nat, R (seq (S i)) (seq i))).
proof: Proof. intros [s Hs]. apply (not_decreasing_aux _ s R Hwf Hs). Qed.
imports: hydras(T1) Coq(Relations)