proposition: Lemma Sumx_minus_Sumx : forall n f g, Sumx n f[-]Sumx n g [=] Sumx _ (fun i Hi => f i Hi[-]g i Hi).
proof: Proof. intros n f g; unfold cg_minus in |- *. eapply eq_transitive_unfolded. 2: apply Sumx_plus_Sumx with (f := f) (g := fun i (Hi : i < n) => [--] (g i Hi)). apply bin_op_wd_unfolded; algebra. apply inv_Sumx. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)