proposition: Lemma poly_01_degree : forall n i, i <= n -> degree_le 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_c_. cut (i = 0). intro. elim (y H0). auto with arith. simpl in |- *. elim (eq_nat_dec i (S n0)); intro. apply degree_le_wd with (poly_01 i n0). algebra. apply poly_01_degree'. pattern (S n0) at 1 in |- *. replace (S n0) with (1 + n0). apply degree_le_mult. apply poly_01_factor_degree. apply Hrecn0. elim (le_lt_eq_dec _ _ H); auto with arith. intro; elim (b b0). auto. Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation