proposition: Theorem gaussian_elimination {m n} (A : Matrix F m n) : ∑ (B : Matrix F _ _), (@matrix_inverse F _ B) × (is_row_echelon (B ** A)).
proof: Proof. destruct (natchoice0 n) as [eq0 | gt]. { now apply gaussian_elimination_width_0. } exists (@gauss_clear_all_rows_as_left_matrix m n A gt). use tpair. { apply gauss_clear_all_rows_matrix_invertible. } rewrite gauss_clear_all_rows_as_matrix_eq; try assumption. now apply gauss_clear_all_rows_inv3. 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