{R : Ring@{i}} {n : nat} (v w : Vector R n) : matrix_plus (matrix_diag v) (matrix_diag w) = matrix_diag (vector_plus v w). Proof. symmetry. snrapply path_matrix. intros i j Hi Hj. rewrite 2 entry_Build_Matrix, 5 entry_Build_Vector. nrapply rng_dist_l. 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.