WIP: select True values in nat predicate.

Lebesgue/nat_compl.v

@@ -41,7 +41,7 @@ Proof.
 intros; lia.
 Qed.
 
-Fixpoint max_n (f : nat -> nat) n :=
+Fixpoint max_n (f : nat -> nat) (n : nat) : nat :=
   match n with
   | 0 => f 0%nat
   | S n => max (f (S n)) (max_n f n)
@@ -83,6 +83,20 @@ Section Select_in_predicate.
 
 Variable P : nat -> Prop. (* Predicate on natural numbers. *)
 
+(*
+Lemma classic_P : forall P (n : nat), P n \/ ~ P n.
+Proof.
+intros; apply classic.
+Qed.
+
+Fixpoint select (P : nat -> Prop) (n : nat) : nat :=
+  match (LPO P (classic_P P)) with
+  | inleft H =>
+    let N := proj1_sig H in N
+  | inright H => 0
+  end.
+*)
+
 Definition useful_finite : (nat -> nat) -> nat -> Prop :=
   fun phi N =>
     (forall n, n < S N -> P (phi n)) /\
@@ -93,9 +107,9 @@ Definition useful_seq : (nat -> nat) -> Prop :=
     (forall n, P (phi n)) /\
     (forall p, P p -> exists n, p = phi n).
 
+(* When we don't need an injecive function fhi *)
 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. *)*)
     match optN with
     | Some N => useful_finite phi N
     | None => useful_seq phi
@@ -105,12 +119,6 @@ destruct (LPO (fun N => forall n, N < n -> ~ P n)) as [[N HN] | H].
 intros; apply classic.
 (* *)
 
-
-
-
-
-
-
 Admitted.
 
 Definition get_useful :