no goals
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ Polynomial.comp (bernsteinPolynomial R n ν) (1 - X) = bernsteinPolynomial R n (n - ν)
simp [bernsteinPolynomial, h, tsub_tsub_assoc, mul_right_comm]