proposition: Lemma Sum2_minus_Sum2 : forall m n, m <= S n -> forall f g, Sum2 m n f[-]Sum2 m n g [=] Sum2 _ _ (fun i Hm Hn => f i Hm Hn[-]g i Hm Hn).
proof: Proof. intros m n H f g; unfold cg_minus in |- *. eapply eq_transitive_unfolded. 2: apply Sum2_plus_Sum2 with (f := f) (g := fun i (Hm : m <= i) (Hn : i <= n) => [--] (g i Hm Hn)); assumption. apply bin_op_wd_unfolded. algebra. apply inv_Sum2; assumption. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)