English
For every integer m, preNormEDS(b,c,d)(2m+1) equals preNormEDS(b,c,d)(m+2) · preNormEDS(b,c,d)(m)^3 · (if Even m then b else 1) minus preNormEDS(b,c,d)(m-1) · preNormEDS(b,c,d)(m+1)^3 · (if Even m then 1 else b).
Русский
Для целого m выполняется: preNormEDS(b,c,d)(2m+1) = preNormEDS(b,c,d)(m+2) · preNormEDS(b,c,d)(m)^3 · (если у m чётное, то b иначе 1) − preNormEDS(b,c,d)(m−1) · preNormEDS(b,c,d)(m+1)^3 · (если чётное m, то 1 иначе b).
LaTeX
$$$$\text{preNormEDS}(b,c,d,2m+1) = \text{preNormEDS}(b,c,d,m+2) \cdot \text{preNormEDS}(b,c,d,m)^3 \cdot (\text{If Even } m \text{ then } b \text{ else } 1) \\ - \text{preNormEDS}(b,c,d,m-1) \cdot \text{preNormEDS}(b,c,d,m+1)^3 \cdot (\text{If Even } m \text{ then } 1 \text{ else } b).$$$$
Lean4
theorem preNormEDS_odd (m : ℤ) :
preNormEDS b c d (2 * m + 1) =
preNormEDS b c d (m + 2) * preNormEDS b c d m ^ 3 * (if Even m then b else 1) -
preNormEDS b c d (m - 1) * preNormEDS b c d (m + 1) ^ 3 * (if Even m then 1 else b) :=
by
induction m using Int.negInduction with
| nat m =>
rcases m with _ | _ | _
iterate 2 simp
simp_rw [Nat.cast_succ, Int.add_sub_cancel, Int.even_add_one, not_not, Int.even_coe_nat]
norm_cast
simpa only [preNormEDS_ofNat] using preNormEDS'_odd ..
| neg ih m =>
rcases m with _ | m
· simp
simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl, show -(m + 1 : ℤ) + 2 = -(m - 1) by ring1,
show -(m + 1 : ℤ) - 1 = -(m + 2) by rfl, show -(m + 1 : ℤ) + 1 = -m by ring1, preNormEDS_neg, even_neg,
Int.even_add_one, ite_not, ih]
ring1
