proposition: Lemma leading_coefficient (p: cpoly CRasCRing): @CPoly_ApZero.interpolates_economically CRasCField crpoints p → nth_coeff (length (tl qpoints)) p == divdiff qpoints.
proof: Proof. Proof with auto. intros. rewrite <- coincides_with_polynomial_interpolators... apply N_leading_coefficient. Qed.
imports: CoRN.model.totalorder.QposMinMax Unicode.Utf8 Setoid Arith List Program Permutation metric2.Classified CSetoids CPoly_ApZero CPoly_Degree CRArith CRArith_alg Qmetric Qring CReals Ranges stdlib_omissions.Pair stdlib_omissions.Q list_separates SetoidPermutation CRings