proposition: Lemma Sumx_Sum0 : forall n f g, (forall i Hi, f i Hi [=] g i) -> Sumx n f [=] Sum0 n g.
proof: Proof. intro; induction n as [| n Hrecn]; simpl in |- *; algebra. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)