proposition: 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: 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.
imports: UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Tactics UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.Matrix UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices UniMath.Algebra.GaussianElimination.Elimination