{R : Ring@{i}} {n : nat} (i j : nat) (Hi : (i < n.+1)%nat) (Hj : (j < n.+1)%nat) (M N : Matrix R n.+1 n.+1) : matrix_minor i j (matrix_plus M N) = matrix_plus (matrix_minor i j M) (matrix_minor i j N). Proof. apply path_matrix. intros k l Hk Hl. by rewrite !entry_Build_Matrix, !entry_Build_Vector. 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.