proposition: Lemma reformulate_final_prop_strong {A : Type} (P : nat -> (nat -> A) -> Prop) (seq : nat -> A) : (forall k : nat, forall l : nat, l <= k -> P l seq) -> (forall k : nat, P k seq).
proof: Proof. intros H k. assert (k <= k) as k_le_k by lia. exact (H k k k_le_k). Qed.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric