proposition: Lemma poly_01_zero : forall n i j, j <= n -> j <> i -> (poly_01 i n) ! (a_ j) [=] [0].
proof: Proof. intros. induction n0 as [| n0 Hrecn0]; intros. rewrite (proj1 (Nat.le_0_r j) H). rewrite (proj1 (Nat.le_0_r j) H) in H0. simpl in |- *. elim (eq_nat_dec i 0); intro y. rewrite y in H0. elim (H0 (refl_equal 0)). astepl ((poly_01_factor 0 i y) ! (a_ 0) [*][1] ! (a_ 0)). astepl ((poly_01_factor 0 i y) ! (a_ 0) [*][1]). astepl (poly_01_factor 0 i y) ! (a_ 0). apply poly_01_factor_zero. elim (eq_nat_dec j (S n0)); intro y. simpl in |- *. rewrite <- y. elim (eq_nat_dec i j); intro y0. rewrite y0 in H0. elim (H0 (refl_equal j)). astepl ((poly_01_factor j i y0) ! (a_ j) [*] (poly_01 i n0) ! (a_ j)). Step_final ([0][*] (poly_01 i n0) ! (a_ j)). cut (j <= n0). intro. simpl in |- *. elim (eq_nat_dec i (S n0)); intro y0. astepl ([1] ! (a_ j) [*] (poly_01 i n0) ! (a_ j)). Step_final ([1] ! (a_ j) [*][0]). astepl ((poly_01_factor (S n0) i y0) ! (a_ j) [*] (poly_01 i n0) ! (a_ j)). Step_final ((poly_01_factor (S n0) i y0) ! (a_ j) [*][0]). elim (le_lt_eq_dec _ _ H); auto with arith. intro; elim (y b). Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation