Lemma matrix_left_inverse_implies_right { n : nat } (A B: Matrix F n n) : (B ** A) = (@identity_matrix F n) -> (@matrix_right_inverse F n n A). Proof. intros ?. destruct (natchoice0 n) as [eq0 | gt]. { destruct eq0; now use tpair. } pose (C := pr1 (gaussian_elimination _ A)). pose (is_gauss := pr2 (gaussian_elimination _ A)). destruct is_gauss as [inv is_re]. pose (CA := C ** A). pose (D := @upper_triangular_right_inverse_construction _ CA). exists (D ** C). assert (CA_ut : is_upper_triangular CA). { apply (@row_echelon_to_upper_triangular _ _ _ CA), is_re. } assert (nonz : @diagonal_all_nonzero F _ CA). { apply left_invertible_upper_triangular_to_diagonal_all_nonzero; try assumption. apply left_inv_matrix_prod_is_left_inv. - exists (pr1 inv). apply (pr2 (pr2 inv)). - now exists B. } pose (invmat := @matrix_right_inverse_construction_inv _ _ CA_ut nonz). unfold CA in invmat. rewrite matrix_mult_assoc in invmat. assert (eq : (C ** A ** D) = (A ** D ** C)). { unfold CA in invmat. unfold D, CA. rewrite matrix_mult_assoc, invmat. pose (left_inv_eq_right := @matrix_left_inverse_equals_right_inverse). apply pathsinv0. pose (gauss_mat_invertible := inv). apply (matrix_inverse_to_right_and_left_inverse) in gauss_mat_invertible. destruct gauss_mat_invertible as [gauss_mat gauss_mat_invertible]. pose (left_inv_eq_right_app := left_inv_eq_right F n _ n C gauss_mat ((A ** D),, invmat)). set (constr := (upper_triangular_right_inverse_construction (@matrix_mult F _ _ C _ A))). assert (eq: (@matrix_mult F _ _ A n constr) = (pr1 gauss_mat)). { apply pathsinv0. apply (left_inv_eq_right_app). } rewrite eq. apply gauss_mat. } refine (_ @ invmat); rewrite <- matrix_mult_assoc; refine (!eq @ _). apply matrix_mult_assoc. Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Nat. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors. Require Import UniMath.Algebra.GaussianElimination.Matrices. Require Import UniMath.Algebra.GaussianElimination.Elimination.