English
For any p and n, the value of the coefficient under a decided condition equals coeff p n: if I is the decidability of n < natDegree p + 1, then ite (n < 1 + natDegree p) (coeff p n) 0 = coeff p n.
Русский
Для любых p и n выражение условия выбора коэффициента равно coeff p n: если I — решение вопроса n < natDegree p + 1, то ite (n < 1 + natDegree p) (coeff p n) 0 = coeff p n.
LaTeX
$$$ p \in R[X], n \in \mathbb{N}, I : \mathrm{Decidable}(n < 1 + \operatorname{natDegree}(p)) \Rightarrow \operatorname{ite}(n < 1 + \operatorname{natDegree}(p)) (p.coeff(n)) 0 = p.coeff(n) $$$
Lean4
theorem ite_le_natDegree_coeff (p : R[X]) (n : ℕ) (I : Decidable (n < 1 + natDegree p)) :
@ite _ (n < 1 + natDegree p) I (coeff p n) 0 = coeff p n :=
by
split_ifs with h
· rfl
· exact (coeff_eq_zero_of_natDegree_lt (not_le.1 fun w => h (Nat.lt_one_add_iff.2 w))).symm
