Exists rel Series is Interval Semistable

theorem exists_relSeries_isIntervalSemistable{ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ] [WellFoundedGT ℒ]{S : Type*} [CompleteLattice S](μ : {p :ℒ × ℒ // p.1 < p.2} → S)[hμ : μA_DescendingChainCondition μ] [hμcvx : Convex μ] [h : μ_Admissible μ] :------------∃ s : RelSeries (IntervalSemistableRel μ),  s.head = ⊥ ∧ s.last = ⊤ ∧  ∀ i : ℕ, (hi : i + 1 < s.length) →    ¬   μA μ ⟨(s.toFun i, s.toFun ↑(i+1)), impl.relSeries_step_lt s hi⟩      ≤ μA μ ⟨(s.toFun ↑(i+1), s.toFun ↑(i+2)), impl.relSeries_succ_step_lt s hi⟩------------ := by  let HNfil : HarderNarasimhanFiltration μ := default  let HNseq : RelSeries (IntervalSemistableRel μ) := {    toFun := fun n ↦ HNfil.filtration n,    length := Nat.find HNfil.fin_len    step := fun i ↦ ⟨HNfil.strict_mono i.val (i.succ).val (Nat.lt_add_one i.val) <|      Fin.is_le i.succ, HNfil.piecewise_semistable i.val i.prop⟩  }  use HNseq  refine ⟨rfl,Nat.find_spec HNfil.fin_len,?_⟩  refine fun i hi hc ↦ HNfil.μA_pseudo_strict_anti i hi ?_  convert hc  · exact Eq.symm (Nat.mod_eq_of_lt <| lt_trans (Nat.lt_add_one i) <|lt_trans hi (Nat.lt_add_one _))  · exact Eq.symm (Nat.mod_eq_of_lt <| lt_trans hi (Nat.lt_add_one _))  · exact Eq.symm (Nat.mod_eq_of_lt <| lt_trans hi (Nat.lt_add_one _))  · exact Eq.symm (Nat.mod_eq_of_lt <| Nat.succ_lt_succ hi)