proposition: Lemma not_decreasing_aux : ~ (forall n:nat, R (seq (S n)) (seq n)).
proof: Proof. unfold not in |- *; intro dec. cut (forall a:A, is_in_seq a -> ~ Acc R a). intro H. absurd (Acc R (seq 0)). apply H. exists 0; trivial. apply W. intro a; pattern a in |- *. apply well_founded_ind with A R. assumption. intros x Hx H. elim H. intros i egi. cut (R (seq (S i)) (seq i)). intro H1. rewrite egi. apply not_acc with (seq (S i)); auto. apply Hx. rewrite egi; auto. exists (S i); auto. auto. Qed.
imports: Relations