Lemma left_invertible_upper_triangular_to_diagonal_all_nonzero {n : nat } (A : Matrix F n n) (p : @is_upper_triangular F _ _ A) (p': @matrix_left_inverse F _ _ A) : (@diagonal_all_nonzero F _ A). Proof. destruct (@vector_all_nonzero_compute_internal _ _ (@diagonal_sq F _ A)) as [l | r]. { unfold diagonal_all_nonzero; intros; unfold diagonal_sq in l; apply l. } unfold diagonal_sq in r; apply fromempty; now apply (@back_sub_zero _ _ A p). 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.