proposition: Lemma Sum2_plus_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 Sum2 in |- *; simpl in |- *. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. 2: apply Sum_plus_Sum. apply Sum_wd; intro i. elim le_lt_dec; intro H0; simpl in |- *; elim le_lt_dec; intro H1; simpl in |- *; algebra. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)