Definition gauss_clear_row_as_left_matrix { m n : nat } (mat : Matrix F m n) (row : (⟦ m ⟧%stn)) (p : n > 0) : Matrix F m m. Proof. destruct (select_uncleared_column F mat row p) as [[piv_col [_ [piv_row _]]] | none]. 2 : {exact (@identity_matrix F _). } set (mat_by_normal_op := (@switch_row F _ _ row piv_row mat)). refine ((gauss_clear_column_as_left_matrix (m,, natgthsnn _) mat_by_normal_op row piv_col) ** _). refine (@switch_row_matrix _ _ row piv_row). 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.