Let R be a ring, and let R[x] be the
polynomials over this ring.
Variable R : CRing.
Fixpoint monom (a : R) (n : N) {struct n} : cpoly_cring R :=
match n with
| O => cpoly_linear _ a (cpoly_zero _)
| S m => cpoly_linear _ 0 (monom a m)
end.
Lemma monom_coeff : forall (c : R) n, nth_coeff n (monom c n) [=] c.
Lemma monom_coeff' : forall (c : R) m n, m <> n -> nth_coeff n (monom c m) [=] 0.
Lemma monom_degree : forall (a : R) n, degree_le n (monom a n).
Lemma monom_S : forall (a : R) n, monom a (S n) [=] _X_[*]monom a n.
Lemma monom_wd_lft : forall (a b : R) n, a [=] b -> monom a n [=] monom b n.
Lemma monom_mult' : forall (a b : R) n, _C_ a[*]monom b n [=] monom (a[*]b) n.
Lemma monom_mult : forall (a b : R) m n,
monom a m[*]monom b n [=] monom (a[*]b) (m + n).
Lemma monom_sum : forall (p : R[x]) n,
degree_le n p -> p [=] ∑ 0 n (fun i => monom (nth_coeff i p) i).
End Monomials.
Section Poly_Reverse.
Variable R : CRing.
Definition Rev (n : N) (p : R[x]) :=
∑ 0 n (fun i => monom (nth_coeff i p) (n - i)).
Lemma Rev_coeff : forall n p i, i <= n -> nth_coeff i (Rev n p) [=] nth_coeff (n - i) p.
Lemma Rev_coeff' : forall n p i, n < i -> nth_coeff i (Rev n p) [=] 0.
Lemma Rev_wd : forall n p p', degree_le n p -> p [=] p' -> Rev n p [=] Rev n p'.
Lemma Rev_rev : forall n p, degree_le n p -> Rev n (Rev n p) [=] p.
Lemma Rev_degree_le : forall n p, degree_le n (Rev n p).
Lemma Rev_degree : forall n p, p ! 0 [#] 0 -> degree n (Rev n p).
Lemma Rev_monom : forall (c : R) m n, m <= n -> Rev n (monom c m) [=] monom c (n - m).
Lemma Rev_zero : forall n, Rev n 0 [=] (0:RX).
Lemma Rev_plus : forall p1 p2 n, Rev n (p1[+]p2) [=] Rev n p1[+]Rev n p2.
Lemma Rev_minus : forall p1 p2 n, Rev n (p1[-]p2) [=] Rev n p1[-]Rev n p2.
Lemma Rev_sum0 : forall a_ l n, Rev n (∑0 l a_) [=] ∑0 l (fun i => Rev n (a_ i)).
Lemma Rev_sum : forall a_ k l n, Rev n (∑ k l a_) [=] ∑ k l (fun i => Rev n (a_ i)).
Lemma Rev_mult : forall n1 n2 p1 p2, degree_le n1 p1 -> degree_le n2 p2 ->
Rev (n1 + n2) (p1[*]p2) [=] Rev n1 p1[*]Rev n2 p2.
End Poly_Reverse.