fact: Definition decreasing_sequence_property := forall a:nat->T, exists n:nat, ~ R (a (S n)) (a n).
imports: Classical Ensembles EnsemblesImplicit Relation_Definitions Relation_Definitions_Implicit EnsemblesSpec ClassicalChoice