Monotony is actually useless!

Lebesgue/Subset_R.v

@@ -568,7 +568,7 @@ destruct HA as [a [b HA]]; rewrite HA.
 unfold union_seq; apply open_or_count; intros n; apply open_intoo.
 (* *)
 destruct (R_second_countable_alt A HA) as [P HP].
-destruct (keep_useful P) as [phi [optN [Hphi HB]]].
+destruct (keep_useful P) as [phi [optN HB]].
 pose (a := get_useful (fun n => fst (bij_NQ2 n)) 0 phi optN).
 pose (b := get_useful (fun n => snd (bij_NQ2 n)) 0 phi optN).
 exists a, b.

Lebesgue/nat_compl.v

@@ -79,7 +79,7 @@ Qed.
 End Even_compl.
 
 
-Section Select_in_pred.
+Section Select_in_predicate.
 
 Variable P : nat -> Prop. (* Predicate on natural numbers. *)
 
@@ -95,7 +95,7 @@ Definition useful_seq : (nat -> nat) -> Prop :=
 
 Lemma keep_useful :
   exists (phi : nat -> nat) (optN : option nat),
-    (forall n1 n2, n1 < n2 -> phi n1 < phi n2) /\ (* phi injective would be fine too. *)
+(*    (forall n1 n2, n1 < n2 -> phi n1 < phi n2) /\ (* phi injective would be fine too. *)*)
     match optN with
     | Some N => useful_finite phi N
     | None => useful_seq phi
@@ -125,7 +125,7 @@ Definition get_useful :
     | None => f (phi n)
     end.
 
-End Select_in_pred.
+End Select_in_predicate.
 
 
 Section Mult_compl.