proposition: Lemma Sum_empty : forall n f, 0 < n -> Sum n (pred n) f [=] [0].
proof: Proof. intros n f H. unfold Sum in |- *. rewrite <- (Nat.lt_succ_pred _ _ H). unfold Sum1 in |- *; algebra. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)