proposition: Lemma reformulate_base_prop_strong {A : Type} (P : nat -> (nat -> A) -> Prop) (seq : nat -> A) : (P 0 seq) -> (forall l : nat, l <= 0 -> P l seq).
proof: Proof. intros H0 l l_le_0. assert (l = 0) as l_eq_0 by lia. rewrite l_eq_0; exact H0. Qed.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric