proposition: Lemma gauss_clear_column_as_left_matrix_inv0 { m n : nat } (iter : stn (S m)) (mat : Matrix F m n) (k_i : (⟦ m ⟧%stn)) (k_j : (stn n)) (i : ⟦ m ⟧%stn) (i_leh_k : i ≤ k_i) : (gauss_clear_column_as_left_matrix iter mat k_i k_j ** mat) i = mat i.
proof: Proof. unfold gauss_clear_column_as_left_matrix. destruct iter as [iter p]. induction iter as [| iter IH]; intros. { simpl; now rewrite matlunax2. } unfold gauss_clear_column_as_left_matrix. rewrite nat_rect_step. destruct (natgthorleh iter k_i) as [gt | _]. 2: { rewrite matlunax2; now rewrite IH. } assert (lt: iter < S m). { apply (istransnatlth _ _ _ (natgthsnn iter) p). } rewrite <- (IH lt). rewrite IH, matrix_mult_assoc, add_row_mult_as_matrix. 2: { now apply issymm_natneq, natgthtoneq. } rewrite add_row_mult_nontarget_row. 2: { apply natgthtoneq. apply (natlehlthtrans _ _ _ i_leh_k gt). } now rewrite IH. 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