proposition: 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: Proof. do 2 rewrite scalar_mult_matrix_product. apply maponpaths, (rigcomm2 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