Lemma clear_row_eq_matrix_def { m n : nat } (mat : Matrix F m n) (r : ⟦ m ⟧%stn) (p : n > 0): ((gauss_clear_row_as_left_matrix mat r p) ** mat) = gauss_clear_row mat r. Proof. intros. unfold gauss_clear_row, gauss_clear_row_as_left_matrix. destruct (natchoice0 _) as [contr_eq | gt]. { apply fromempty; rewrite contr_eq in p; contradiction (isirreflnatgth _ p). } assert (eq : p = gt). { apply propproperty. } rewrite eq. destruct (select_uncleared_column F mat r _). 2: {apply matlunax2. } now rewrite matrix_mult_assoc, switch_row_as_matrix, clear_column_eq_matrix_def. 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.