proposition: Lemma Rev_zero : forall n, Rev n [0] [=] ([0]:RX).
proof: Proof. intros. apply all_nth_coeff_eq_imp. intros. elim (le_lt_dec i n); intros. astepl (nth_coeff (n - i) [0]:R). Step_final ([0]:R). Step_final ([0]:R). Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)