proposition: Lemma row_vec_col_vec_mult_eq {m n} (A : Matrix CR m n) (x : Vector CR n) : transpose ((row_vec x) ** (transpose A)) = A ** (col_vec x).
proof: Proof. etrans. { apply matrix_product_transpose. } apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors