proposition: Lemma Rev_sum0 : forall a_ l n, Rev n (Sum0 l a_) [=] Sum0 l (fun i => Rev n (a_ i)).
proof: Proof. intros. induction l as [| l Hrecl]. replace (Sum0 0 a_) with ([0]:RX). replace (Sum0 0 (fun i : nat => Rev n (a_ i))) with ([0]:RX). algebra. auto. auto. replace (Sum0 (S l) a_) with (Sum0 l a_[+]a_ l). replace (Sum0 (S l) (fun i : nat => Rev n (a_ i))) with (Sum0 l (fun i : nat => Rev n (a_ i)) [+]Rev n (a_ l)). astepl (Rev n (Sum0 l a_) [+]Rev n (a_ l)). apply bin_op_wd_unfolded. auto. algebra. auto. auto. Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)