Lemma scalar_mult_matrix_one {n : nat} (r : ⟦ n ⟧%stn) : scalar_mult_row_matrix r (@rigunel2 F) = @identity_matrix F _. Proof. unfold scalar_mult_row_matrix. apply funextfun; intros i. destruct (stn_eq_or_neq i r); simpl coprod_rect. 2: { reflexivity. } apply funextfun; intros j. apply (@riglunax2 F). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors. Require Import UniMath.Algebra.GaussianElimination.Matrices.