proposition: Lemma not_decreasing_aux : ~ (forall n:nat, R (seq (S n)) (seq n)).
proof: Proof. unfold not in |- *; intro Hseq. assert (H : forall a:A, is_in_seq a -> ~ Acc R a). - intro a; pattern a in |- *; apply well_founded_ind with A R; auto. intros x Hx [i Hi]; generalize (Hseq i); intro H0; rewrite Hi. apply not_acc with (seq (S i)); auto. apply Hx. + rewrite Hi; auto. + exists (S i); auto. - apply (H (seq 0)). + exists 0; trivial. + apply Rwf. Qed.
imports: hydras(T1) Coq(Relations)