proposition: Theorem not_decreasing : ~ (exists seq : nat -> A, (forall i:nat, R (seq (S i)) (seq i))).
proof: 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.
imports: Relations