{R : Ring} {n} (M N : Matrix R n n) : matrix_trace (matrix_plus M N) = (matrix_trace M) + (matrix_trace N). Proof. unfold matrix_trace. lhs nrapply path_ab_sum. { intros i Hi. by rewrite entry_Build_Matrix. } by rewrite ab_sum_plus. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.Decidable. Require Import Types.Sigma. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import Algebra.Rings.Ring Algebra.Rings.Module Algebra.Rings.CRing Require Import abstract_algebra. Require Import WildCat.Core WildCat.Paths. Require Import Modalities.ReflectiveSubuniverse.