proposition: Lemma Rev_degree : forall n p, p ! [0] [#] [0] -> degree n (Rev n p).
proof: Proof. unfold degree_le in |- *. unfold degree in |- *. intros. split. astepl (nth_coeff (n - n) p). replace (n - n) with 0. astepl p ! [0]. auto. auto with arith. apply Rev_degree_le. Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)