Lemma add_row_mult_as_matrix { m n } (r1 r2 : ⟦ m ⟧%stn) (ne : r1 ≠ r2) (s : R) (mat : Matrix R m n) : (add_row_mult_matrix r1 r2 s) **' mat = add_row_mult r1 r2 s mat. Proof. intros. apply funextfun; intros i; apply funextfun; intros j. unfold matrix_mult, add_row_mult_matrix, add_row_mult, col, row. destruct (stn_eq_or_neq i r2) as [i_eq_r2 | i_neq_r2]; simpl coprod_rect. - etrans. { apply maponpaths, (@pointwise_rdistr_vector R). } etrans. { apply vecsum_add. } apply map_on_two_paths. + etrans. 2: { apply maponpaths_2, i_eq_r2. } use sum_stdb_vector_pointwise_prod. + etrans. { apply vecsum_scalar_lmult. } apply maponpaths, @sum_stdb_vector_pointwise_prod. - use sum_stdb_vector_pointwise_prod. 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.