proposition: Lemma Sumx_plus_Sumx : forall n f g, Sumx n f[+]Sumx n g [=] Sumx n (fun i Hi => f i Hi[+]g i Hi).
proof: Proof. intro n; induction n as [| n Hrecn]. intros; simpl in |- *; algebra. intros f g; simpl in |- *. apply eq_transitive_unfolded with (Sumx _ (fun (i : nat) (l : i < n) => f i (Nat.lt_lt_succ_r i n l)) [+] Sumx _ (fun (i : nat) (l : i < n) => g i (Nat.lt_lt_succ_r i n l)) [+] (f n (Nat.lt_succ_diag_r n) [+]g n (Nat.lt_succ_diag_r n))). set (Sf := Sumx _ (fun (i : nat) (l : i < n) => f i (Nat.lt_lt_succ_r i n l))) in *. set (Sg := Sumx _ (fun (i : nat) (l : i < n) => g i (Nat.lt_lt_succ_r i n l))) in *. set (fn := f n (Nat.lt_succ_diag_r n)) in *; set (gn := g n (Nat.lt_succ_diag_r n)) in *. astepl (Sf[+]fn[+]Sg[+]gn). astepl (Sf[+] (fn[+]Sg) [+]gn). astepl (Sf[+] (Sg[+]fn) [+]gn). Step_final (Sf[+]Sg[+]fn[+]gn). apply bin_op_wd_unfolded; algebra. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)