Lemma matrix_right_inverse_construction_inv { n : nat } (mat : Matrix F n n) (ut : @is_upper_triangular F _ _ mat) (df: @diagonal_all_nonzero F _ mat) : (mat ** (upper_triangular_right_inverse_construction mat)) = (@identity_matrix F n). Proof. apply funextfun; intros i. unfold matrix_mult, row, col, transpose, flip. apply funextfun; intros ?. unfold upper_triangular_right_inverse_construction. rewrite (@col_vec_mult_eq F _ _ mat _ (@identity_matrix F _ x)). - destruct (stn_eq_or_neq i x) as [eq | neq]. { now rewrite eq. } rewrite id_mat_ij; try rewrite id_mat_ij; try easy. apply (issymm_natneq _ _ neq). - unfold upper_triangular_right_inverse_construction. pose (back_sub_inv := @back_sub_inv0). destruct (natchoice0 n) as [eq | ?]. {apply fromstn0; now rewrite eq. } apply (back_sub_inv _ _ _ _ ut df). 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.