proposition: Lemma poly_01_factor'_apzero : forall n i, i <> n -> (poly_01_factor' n) ! (a_ i) [#] [0].
proof: Proof. intros. unfold poly_01_factor' in |- *. astepl (_X_ ! (a_ i) [-] (_C_ (a_ n0)) ! (a_ i)). astepl (a_ i[-]a_ n0). algebra. Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation