Print well_founded.

Print  well_founded_ind.

Require Import Relations.

Print inclusion.

Lemma wf_inclusion: forall (A:Set)(R S: A->A->Prop), 
   inclusion A R S ->  well_founded S -> well_founded R.


Require Import Wellfounded.

Theorem not_decreasing: forall (A:Set)(R: A->A->Prop), 
  well_founded R ->
   ~(exists seq:nat->A, (forall i:nat, R (seq(S i)) (seq i))).


(*A co z twierdzeniem odwrotnym ? A w logice klasycznej? *)