fact: Fixpoint poly_01 (i n : nat) {struct n} : cpoly_cring R := match eq_nat_dec i n with | left _ => [1] | right ne => poly_01_factor n i ne end [*] match n with | O => [1] | S m => poly_01 i m end.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation