proposition: 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: 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.
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