proposition: Lemma gauss_clear_column_step_inv1 {m n : nat} (r_pivot : ⟦m⟧%stn) (c_pivot : ⟦ n ⟧%stn) (r : (⟦ m ⟧%stn)) (mat : Matrix F m n) (p_1 : mat r_pivot c_pivot != 0%ring) (p_2 : r ≠ r_pivot) : (gauss_clear_column_step r_pivot c_pivot r mat) r c_pivot = 0%ring.
proof: Proof. intros; unfold gauss_clear_column_step. destruct (stn_eq_or_neq r r_pivot) as [p | _]. { rewrite p in p_2. now apply isirrefl_natneq in p_2. } rewrite add_row_mult_as_matrix. 2: { now apply issymm_natneq. } rewrite add_row_mult_target_row. rewrite <- (@ringlmultminus F), ringassoc2. etrans. { now apply maponpaths, maponpaths, fldmultinvlax'. } rewrite (@rigrunax2 F); apply ringrinvax1. 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