proposition: Lemma poly_01_factor'_degree : forall n, degree_le 1 (poly_01_factor' n).
proof: Proof. intros. unfold poly_01_factor' in |- *. apply degree_imp_degree_le. apply degree_minus_lft with 0. apply degree_le_c_. apply degree_x_. auto. Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation