Lemma identity_matrix {n : nat} : (Matrix R n n). Proof. intros i j. induction (stn_eq_or_neq i j). - exact (rigunel2). - exact (rigunel1). Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.FiniteSequences. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.RigsAndRings.