{R : CRing} {m n : nat} (M : Matrix R m n) (N : Matrix R n m) : matrix_trace (matrix_mult M N) = matrix_trace (matrix_mult N M). Proof. lhs nrapply path_ab_sum. { intros i Hi. lhs nrapply entry_Build_Matrix. nrapply path_ab_sum. intros j Hj. apply rng_mult_comm. } lhs nrapply ab_sum_sum. apply path_ab_sum. intros i Hi. rhs nrapply entry_Build_Matrix. reflexivity. 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.