proposition: 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: 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.
imports: UniMath.Foundations.PartA UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.FiniteSequences UniMath.Combinatorics.Vectors UniMath.Combinatorics.Maybe UniMath.Algebra.BinaryOperations UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.RigsAndRings UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices UniMath.Algebra.GaussianElimination.RowOps