proposition: Lemma zero_poly : forall n, (forall i j: nat, i <= n -> j <= n -> i <> j -> a_ i[#]a_ j) -> forall (f : RX), degree_le n f -> (forall i, i <= n -> f ! (a_ i) [=] [0]) -> f [=] [0].
proof: Proof. Proof with auto. intro. clear degree_f n distinct_a_. intro distinct_a_. induction n0 as [| n0 Hrecn0]; intros. elim (degree_le_zero _ _ H). intros. astepl (_C_ x). astepr (_C_ ([0]:R)). apply cpoly_const_eq. apply eq_transitive_unfolded with f0 ! (a_ 0). Step_final (_C_ x) ! (a_ 0). apply H0... cut (f0 ! (a_ (S n0)) [=] [0])... intro. elim (poly_linear_factor f0 (a_ (S n0)) H1). intro f'. intros. astepl ((_X_[-]_C_ (a_ (S n0))) [*]f'). cut (f' [=] [0]). intro. Step_final ((_X_[-]_C_ (a_ (S n0))) [*][0]). apply Hrecn0. intuition. apply degree_le_mult_imp with (_X_[-]_C_ (a_ (S n0))) 1. apply degree_minus_lft with 0... apply degree_le_c_. apply degree_x_. apply degree_le_wd with f0... intros. apply mult_cancel_lft with (a_ i[-]a_ (S n0)). apply minus_ap_zero. apply distinct_a_... intro; rewrite H3 in H2; exact (Nat.nle_succ_diag_l _ H2). astepr ([0]:R). cut (a_ i[-]a_ (S n0) [=] (_X_[-]_C_ (a_ (S n0))) ! (a_ i)). intro. astepl ((_X_[-]_C_ (a_ (S n0))) ! (a_ i) [*]f' ! (a_ i)). astepl ((_X_[-]_C_ (a_ (S n0))) [*]f') ! (a_ i). astepl f0 ! (a_ i)... Step_final (_X_ ! (a_ i) [-] (_C_ (a_ (S n0))) ! (a_ i)). Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation