Lemma matrix_right_inverse_implies_left { n : nat } (A B: Matrix F n n) : @matrix_right_inverse F _ _ A -> (@matrix_left_inverse F _ _ A). Proof. intros [rinv isrinv]. pose (linv := @make_matrix_left_inverse F _ _ n A rinv isrinv). pose (linv_to_rinv := @matrix_left_inverse_implies_right _ _ _ isrinv). exists rinv. pose (inv_eq := @matrix_left_inverse_equals_right_inverse _ n _ n _ linv linv_to_rinv). simpl in inv_eq; rewrite inv_eq; apply linv_to_rinv. 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.