proposition: Lemma Rev_coeff' : forall n p i, n < i -> nth_coeff i (Rev n p) [=] [0].
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 (R:=R) i0 p) (n - i0)). apply Sum_zero. auto with arith. intros. cut (n - i0 <> i). intro. algebra. lia. Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)