chore(data/polynomial/basic): golf (#17656) Add polynomial.C_injective, golf some proofs

polynomial.C_injective