proposition: Lemma Rev_coeff : forall n p i, i <= n -> nth_coeff i (Rev n p) [=] nth_coeff (n - i) p.
proof: Proof. intros. unfold Rev in |- *. apply eq_transitive_unfolded with (Sum 0 n (fun i0 : nat => nth_coeff i (monom (nth_coeff i0 p) (n - i0)))). apply nth_coeff_sum with (p_ := fun i0 : nat => monom (nth_coeff i0 p) (n - i0)). apply eq_transitive_unfolded with (nth_coeff i (monom (nth_coeff (n - i) p) (n - (n - i)))). apply Sum_term with (i := n - i) (f := fun i0 : nat => nth_coeff i (monom (nth_coeff i0 p) (n - i0))). auto with arith. lia. intros. cut (n - j <> i). intro. algebra. lia. replace (n - (n - i)) with i. algebra. lia. Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)