proposition: Lemma Rev_wd : forall n p p', degree_le n p -> p [=] p' -> Rev n p [=] Rev n 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) p). Step_final (nth_coeff (n - i) p'). Step_final ([0]:R). Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)