proposition: Lemma Rev_sum : forall a_ k l n, Rev n (Sum k l a_) [=] Sum k l (fun i => Rev n (a_ i)).
proof: Proof. intros. unfold Sum in |- *. unfold Sum1 in |- *. astepl (Rev n (Sum0 (S l) a_) [-]Rev n (Sum0 k a_)). apply cg_minus_wd; apply Rev_sum0. Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)