fact: Definition const_seq_from {A : Type} (a : A) (k : nat) (seq : nat -> A) := fun l : nat => if (lt_dec l k) then (seq l) else a.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric