proposition: Lemma exists_max k (P : pos k -> nat -> Prop) : (forall (p:pos k), exists n, P p n) -> exists m, forall (p:pos k), exists n, P p n /\ m >= n.
proof: Proof. intros H. induction k as [|k IH]. - exists 0. intros p. now eapply pos_O_invert. - specialize (IH (fun p n => P (pos_nxt p) n)). cbn in IH. destruct IH as [m1 Hm1]. + intros p. apply H. + destruct (H pos0) as [m2 Hm2]. exists (max m1 m2). apply pos_S_invert. * exists m2. split; now try lia. * intros p. edestruct Hm1 as [m3 [Hm3A Hm3B]]. exists m3; split; try lia. exact Hm3A. Qed.
imports: Arith Lia List Bool Eqdep_dec EqdepFacts Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Undecidability.MuRec.Util.recalg