theorem lemma2_3_3 (P : RateMatrix) (lambdaP : ℕ → ℝ) (h₀ : InvariantDistribution P lambdaP) (n : ℕ) [NeZero n] (n_non_zero : n ≠ 0) (A : Fin n → ℕ) (Indices_props : (∀ (i : ℕ) (h : i < n - 1), A ⟨i, ⋯⟩ < A ⟨i + 1, ⋯⟩) ∧ ∀ (i : ℕ) (h : i < n), A ⟨i, h⟩ ≠ 0 → P.Q (A ⟨i, h⟩) (A ⟨i, h⟩ - 1) = 0) : (∀ (i : ℕ), P.Q i (i + 1) ≠ 0) → (∀ (m : ℕ), m ≠ 0 ∧ P.Q m (m - 1) = 0 → ∃ (i : Fin n), m = A i) → ∀ (i : Fin (A ↑(n - 1))), lambdaP ↑i = 0