proposition: 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: 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.
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