proposition: Lemma poly_01_one : forall n i, (poly_01 i n) ! (a_ i) [=] [1].
proof: Proof. intros. induction n0 as [| n0 Hrecn0]; intros. simpl in |- *. elim (eq_nat_dec i 0); intro y. astepl ([1] ! (a_ i) [*][1] ! (a_ i)). Step_final ([1][*] ([1]:R)). astepl ((poly_01_factor 0 i y) ! (a_ i) [*][1] ! (a_ i)). astepl ((poly_01_factor 0 i y) ! (a_ i) [*][1]). astepl (poly_01_factor 0 i y) ! (a_ i). apply poly_01_factor_one. simpl in |- *. elim (eq_nat_dec i (S n0)); intro y. astepl ([1] ! (a_ i) [*] (poly_01 i n0) ! (a_ i)). astepl ([1][*] (poly_01 i n0) ! (a_ i)). Step_final ([1][*] ([1]:R)). astepl ((poly_01_factor (S n0) i y) ! (a_ i) [*] (poly_01 i n0) ! (a_ i)). astepl ((poly_01_factor (S n0) i y) ! (a_ i) [*][1]). astepl (poly_01_factor (S n0) i y) ! (a_ i). apply poly_01_factor_one. Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation