proposition: Lemma N_leading_coefficient: nth_coeff (length (tl qpoints)) (N qpoints) == divdiff qpoints.
proof: Proof. Proof with try ring. destruct qpoints. change (divdiff (ne_list.one p) * 1 + 0 == divdiff (ne_list.one p))... simpl @length. rewrite N_cons. rewrite nth_coeff_plus. rewrite (degree l (length l)). 2: destruct l; simpl; auto. change (nth_coeff (length l) (an (p ::: l))+0==divdiff (p ::: l)). ring_simplify. unfold an. rewrite nth_coeff_c_mult_p. simpl tl. set (f := fun x: Q and CR => @cpoly_linear_fun' CRasCRing (' (- fst x)%Q) [1]). replace (length l) with (length (map f l) * 1)%nat. rewrite lead_coeff_product_1. change (divdiff (p ::: l)*1 == divdiff (p ::: l))... intros q. rewrite in_map_iff. intros [x [[] B]]. split. reflexivity. apply degree_le_cpoly_linear_inv. apply (degree_le_c_ CRasCRing [1]). rewrite map_length... 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