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