To Out Codewords Count mul ϑ eq i succ

lemma toOutCodewordsCount_mul_ϑ_eq_i_succ (i : Fin ℓ) (hCR : isCommitmentRound ℓ ϑ i) :  (toOutCodewordsCount ℓ ϑ i.castSucc) * ϑ = i.val + 1 := by  unfold toOutCodewordsCount  simp only [Fin.coe_castSucc, i.isLt, ↓reduceIte]  have h_mod : i.val % ϑ = ϑ - 1 := by    refine (mod_eq_sub_iff ?_ ?_).mpr hCR.1    · omega    · exact NeZero.one_le  -- After unfolding, we have: (i.val / ϑ + 1) * ϑ = i.val + 1  rw [Nat.add_mul, one_mul]  -- Now we have: (i.val / ϑ) * ϑ + ϑ = i.val + 1  -- Since ϑ ∣ (i.val + 1), we can use Nat.div_mul_cancel  -- ⊢ ↑i / ϑ * ϑ + ϑ = ↑i + 1  rw [Nat.div_mul_self_eq_mod_sub_self, h_mod]  rw [←Nat.sub_add_comm (k:=ϑ - 1) (m:=ϑ) (by    calc _ = i.val % ϑ := by omega      _ ≤ i := by exact Nat.mod_le (↑i) ϑ  )]  -- ⊢ ↑i + ϑ - (ϑ - 1) = ↑i + 1  rw [Nat.sub_sub_right (a:=i.val + ϑ) (b:=ϑ) (c:=1) (by exact NeZero.one_le)]  omega