proposition: Lemma poly_representation'' : forall (a : nat -> R) i, i <= n -> (forall j, j <> i -> a j [=] [0]) -> Sum 0 n a [=] a i.
proof: Proof. intro. intro. elim i. intros. astepl (a 0[+]Sum 1 n a). astepr (a 0[+][0]). apply bin_op_wd_unfolded. algebra. apply Sum_zero. auto with arith. intros. apply H0. intro; rewrite H3 in H1; inversion H1. intro i'. intros. astepl (Sum 0 i' a[+]Sum (S i') n a). astepr ([0][+]a (S i')). apply bin_op_wd_unfolded. apply Sum_zero. auto with arith. intros. apply H1. intro; rewrite H4 in H3; exact (Nat.nle_succ_diag_l _ H3). astepl (a (S i') [+]Sum (S (S i')) n a). astepr (a (S i') [+][0]). apply bin_op_wd_unfolded. algebra. apply Sum_zero. auto with arith. intros. apply H1. intro; rewrite H4 in H2; exact (Nat.nle_succ_diag_l _ H2). Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation