dist_LTSeries

lemma dist_LTSeries {n : ℕ} {u : Set (𝔓 X)} {s : LTSeries u} (hs : s.length = n) {f g : Θ X} :    dist_(s.head.1) f g ≤ C2_1_2 a ^ n * dist_(s.last.1) f g := by  induction n generalizing s with  | zero => rw [pow_zero, one_mul]; apply Grid.dist_mono s.head_le_last.1  | succ n ih =>    let s' : LTSeries u := s.eraseLast    specialize ih (show s'.length = n by simp [s', hs])    have link : dist_(s'.last.1) f g ≤ C2_1_2 a * dist_(s.last.1) f g :=      Grid.dist_strictMono <| 𝓘_strictMono <| s.eraseLast_last_rel_last (by lia)    apply ih.trans; rw [pow_succ, mul_assoc]; gcongr; unfold C2_1_2; positivity