Definition gauss_clear_column_step {m n : nat} (k_i : (⟦ m ⟧%stn)) (k_j : (⟦ n ⟧%stn)) (i : (stn m)) (mat : Matrix F m n) : Matrix F m n. Proof. destruct (stn_eq_or_neq i k_i). - exact mat. - refine ((@add_row_mult_matrix F _ k_i i _)%ring ** mat). exact (- ((mat i k_j) * fldmultinv' (mat k_i k_j)))%ring. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Nat. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.FiniteSequences. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Matrix. 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. Require Import UniMath.Algebra.GaussianElimination.RowOps.