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