proposition: Lemma scalar_mult_matrix_one {n : nat} (r : ⟦ n ⟧%stn) : scalar_mult_row_matrix r (@rigunel2 F) = @identity_matrix F _.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.Matrix UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices