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