Theorem gaussian_elimination {m n} (A : Matrix F m n) : ∑ (B : Matrix F _ _), (@matrix_inverse F _ B) × (is_row_echelon (B ** A)). 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.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Nat. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.FiniteSequences. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors. Require Import UniMath.Algebra.GaussianElimination.Matrices. Require Import UniMath.Algebra.GaussianElimination.RowOps.