proposition: Lemma Sum_one : forall n f, Sum n n f [=] f n.
proof: Proof. intros n f. unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *. Step_final (f n[+]Sum0 n f[-]Sum0 n f). Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)