proposition: Lemma scalar_mult_as_matrix {m n : nat} (r : ⟦ m ⟧%stn) (s : F) (mat : Matrix F m n) : ((scalar_mult_row_matrix r s) **' mat) = scalar_mult_row r s mat.
proof: Proof. use funextfun; intros i; use funextfun; intros ?. unfold matrix_mult, scalar_mult_row_matrix, scalar_mult_row, row. destruct (stn_eq_or_neq i r) as [? | ?]. - simpl coprod_rect. etrans. { apply maponpaths. etrans. { apply maponpaths_2, (@pointwise_comm2_vector F). } apply pointwise_assoc2_vector. } use sum_stdb_vector_pointwise_prod. - simpl coprod_rect. use sum_stdb_vector_pointwise_prod. 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