Library prelude.not_decreasing

Require Import Relations.
Section Sequences.
 Variable A : Set.

 Variable R : A -> A -> Prop.

 Lemma not_acc : forall a b:A, R a b -> ~ Acc R a -> ~ Acc R b.
 Proof.
  intros a b H H0 H1.
  absurd (Acc R a); auto.
  generalize a H.
  elim H1; auto.
 Qed.

 Lemma acc_imp : forall a b:A, R a b -> Acc R b -> Acc R a.
 Proof.
  intros a b H H0.
  generalize a H.
  elim H0; auto.
 Qed.

 Hypothesis W : well_founded R.
 Hint Resolve W.

 Section seq_intro.
  Variable seq : nat -> A.

  Let is_in_seq (x:A) := exists i : nat, x = seq i.

  Lemma not_decreasing_aux : ~ (forall n:nat, R (seq (S n)) (seq n)).
  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.
 End seq_intro.

 Theorem not_decreasing :
  ~ (exists seq : nat -> A, (forall i:nat, R (seq (S i)) (seq i))).
 Proof.
  unfold not in |- *; intro H.
  case H; intros s Hs.
  absurd (forall i:nat, R (s (S i)) (s i)); auto.
  apply not_decreasing_aux.
 Qed.

End Sequences.