proposition: Lemma WF_implies_DSP: well_founded R -> decreasing_sequence_property.
proof: Proof. unfold decreasing_sequence_property. intros WF a. remember (a 0) as a0. revert a0 a Heqa0. apply (well_founded_ind WF (fun x:T => forall a:nat->T, x = a 0 -> exists n:nat, ~ R (a (S n)) (a n))). intros. case (classic (R (a 1) (a 0))). - intro. pose (b := fun n:nat => a (S n)). assert (exists n:nat, ~ R (b (S n)) (b n)). { apply H with (a 1). - rewrite H0. assumption. - trivial. } destruct H2. exists (S x0). unfold b in H2. assumption. - exists 0. assumption. Qed.
imports: Coq(Classical) ZornsLemma(EnsemblesImplicit) ZornsLemma(Relation_Definitions_Implicit) ZornsLemma(EnsemblesSpec) ClassicalChoice