proposition: Lemma Rev_rev : forall n p, degree_le n p -> Rev n (Rev n p) [=] p.
proof: Proof. unfold RX in |- *. intros. apply all_nth_coeff_eq_imp. intros. elim (le_lt_dec i n); intros. astepl (nth_coeff (n - i) (Rev n p)). pattern i at 2 in |- *. replace i with (n - (n - i)). apply Rev_coeff. lia. lia. unfold degree_le in H. Step_final ([0]:R). Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)