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