proposition: Lemma poly_01_degree' : forall n i, degree_le (S n) (poly_01 i n).
proof: Proof. intros. induction n0 as [| n0 Hrecn0]. intros. simpl in |- *. elim (eq_nat_dec i 0); intro y. apply degree_le_wd with (_C_ ([1]:R)). Step_final ([1]:cpoly_cring R). apply degree_le_mon with 0. auto with arith. apply degree_le_c_. apply degree_le_wd with (poly_01_factor 0 i y). algebra. apply poly_01_factor_degree. simpl in |- *. elim (eq_nat_dec i (S n0)); intro. apply degree_le_mon with (S n0). auto. apply degree_le_wd with (poly_01 i n0). algebra. auto. replace (S (S n0)) with (1 + S n0). apply degree_le_mult. apply poly_01_factor_degree. auto. auto. Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation