Lemma scalar_mult_matrix_comm { n : nat } ( r : ⟦ n ⟧%stn ) ( s1 s2 : F ) : ((scalar_mult_row_matrix r s1) **' (scalar_mult_row_matrix r s2)) = ((scalar_mult_row_matrix r s2) **' (scalar_mult_row_matrix r s1)). Proof. do 2 rewrite scalar_mult_matrix_product. apply maponpaths, (rigcomm2 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.