# Library Cantor.prelude.not_decreasing

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

Variable R : A A Prop.

Lemma not_acc : 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 : 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) := i : nat, x = seq i.

Lemma not_decreasing_aux : ¬ ( n:nat, R (seq (S n)) (seq n)).
Proof.
unfold not in |- *; intro dec.
cut ( a:A, is_in_seq a ¬ Acc R a).
intro H.
absurd (Acc R (seq 0)).
apply H.
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.
(S i); auto.
auto.
Qed.
End seq_intro.

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

End Sequences.