proposition: Lemma Rev_monom : forall (c : R) m n, m <= n -> Rev n (monom c m) [=] monom c (n - m).
proof: Proof. intros. apply all_nth_coeff_eq_imp. intros. elim (le_lt_dec i n); intro y. astepl (nth_coeff (n - i) (monom c m)). elim (eq_nat_dec m (n - i)); intro H0. cut (i = n - m). intro y0. rewrite <- y0. rewrite H0. Step_final c. lia. cut (n - m <> i). intro. Step_final ([0]:R). lia. cut (n - m <> i). intro. Step_final ([0]:R). lia. Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)