proposition: Lemma Sum_last' : forall m n f, 0 < n -> Sum m n f [=] Sum m (pred n) f[+]f n.
proof: Proof. intros m n f H. induction n as [| n Hrecn]. elim (Nat.lt_irrefl 0 H). apply Sum_last. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)