Lemma gauss_clear_column_as_left_matrix { m n : nat } (iter : ⟦ S m ⟧%stn) (mat : Matrix F m n) (k_i : (⟦ m ⟧%stn)) (k_j : (⟦ n ⟧%stn)) : Matrix F m m. Proof. destruct iter as [iter p]. generalize p; intros lt; clear p. induction iter as [| iter IH]. {exact (@identity_matrix F m). } assert (p': iter < S m). { apply (istransnatlth _ _ _ (natgthsnn iter) lt). } destruct (natgthorleh iter k_i). 2: { exact (@identity_matrix F m ** (IH p')). } refine (@add_row_mult_matrix F _ k_i (iter,, lt) (- (_ * _))%ring ** _). - exact (mat (iter,, lt) k_j). - exact (fldmultinv' (mat k_i k_j)). - exact (IH p'). 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.