proposition: Lemma Cpoly_choose_apzero : f [#] [0] -> {i : nat | i <= n | f ! (a_ i) [#] [0]}.
proof: Proof. intros H. cut (Sum 0 n (fun i : nat => _C_ f ! (a_ i) [*]poly_01 i n) [#] [0]). intros H0. elim (Sum_apzero _ (fun i : nat => _C_ f ! (a_ i) [*]poly_01 i n) 0 n ( Nat.le_0_l n) H0). intro i. intro H1. elim H1. intros H2 H3. intro H4. exists i. auto. apply poly_c_apzero. apply cring_mult_ap_zero with (poly_01 i n). auto. astepl f. auto. Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation