proposition: Lemma mu_least (p : nat -> Prop) (d : forall x, dec (p x)) (H : ex p) : forall n, p n -> mu' d H <= n.
proof: Proof. intros n H'. destruct (Nat.le_gt_cases (mu' d H) n) as [Hl | Hl]; eauto. exfalso. enough (mu' d H <= n) by lia. eapply rel_ls_lower_bound with (start := 0); eauto with arith. unfold mu, constructive_indefinite_ground_description_nat. now destruct linear_search_from_0_conform. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia