proposition: Lemma back_sub_zero { n : nat } (mat : Matrix F n n) (ut : @is_upper_triangular F _ _ mat) (zero: ∑ i : stn n, (mat i i = 0)%ring × (forall j : stn n, j < i -> ((mat j j) != 0)%ring)) (inv : @matrix_left_inverse F _ _ mat) : empty.
proof: Proof. unfold transpose, flip. destruct (natchoice0 (pr1 zero)) as [eq0_1 | gt]. { apply (zero_row_to_non_right_invertibility (transpose mat) (pr1 zero)); try assumption. 2: { now apply (@matrix_left_inverse_to_transpose_right_inverse F). } apply funextfun; intros k. destruct (natchoice0 k) as [eq0_2 | ?]. - rewrite <- (pr1 (pr2 zero)). unfold const_vec. rewrite eq0_1 in eq0_2. now rewrite (stn_eq _ _ eq0_2). - unfold transpose, flip. rewrite ut; try reflexivity. now rewrite <- eq0_1. } assert (contr_exists : ∑ x : (Vector F n), (∑ i' : stn n, (x i' != 0) × (mat ** (col_vec x)) = (@col_vec F _ (const_vec 0)))). 2: { assert (eqz : (mat ** (@col_vec F _ (const_vec 0))) = (@col_vec F _ (const_vec 0))). { rewrite matrix_mult_eq; unfold matrix_mult_unf. apply funextfun; intros k. unfold col_vec, const_vec. etrans. { rewrite vecsum_eq_zero. - apply idpath. - intros ?; apply rigmultx0. } reflexivity. } assert (contr_eq' : (@ringunel1 F) != (@ringunel1 F)). 2: { contradiction. } rewrite <- eqz in contr_exists. destruct contr_exists as [x1 [x2 [x3 contr_exists]]]. destruct inv as [inv isinv]. rewrite <- contr_exists in eqz. assert (eq : @matrix_mult F _ _ inv _ (@matrix_mult F _ _ mat _ (col_vec x1)) = @matrix_mult F _ _ inv _ (@col_vec F _ (const_vec 0))). { now rewrite eqz. } rewrite <- matrix_mult_assoc, isinv, matlunax2 in eq. pose (eq' := @matrix_mult_zero_vec_eq _ _ _ inv). unfold col_vec, const_vec in * |-. rewrite eq' in eq. destruct zero as [zero iszero]. apply toforallpaths in eq. set (idx0 := (make_stn _ 0 (stn_implies_ngt0 zero))). assert (contr_eq' : (λ (_ : _) (_ : _), (@rigunel1 F)) idx0 = (λ (_ : _) (_ : (⟦ 1 ⟧)%stn), x1 x2) idx0 ). { now rewrite eq. } apply toforallpaths in contr_eq'. rewrite contr_eq' in x3. 2: { exact (make_stn _ _ (natgthsnn 0)). } contradiction. } destruct zero as [zero iszero]. use tpair. { apply back_sub_internal. - exact mat. - intros j. destruct (natlthorgeh (pr1 zero) j). + exact 0. + destruct (natgehchoice (pr1 zero) j); try assumption. * exact 0. * exact (@rigunel2 F). - exact (const_vec 0). - exact (n,, natgthsnn _). - exact (pr1 zero,, (istransnatlth _ _ _ (pr2 zero) (natgthsnn _))). } exists zero. use tpair. - rewrite back_sub_internal_inv1; try assumption. 2: { apply isreflnatleh. } destruct (natlthorgeh _ _) as [lt | ge]. * contradiction (isirreflnatgth _ lt). * simpl; clear gt. destruct (natgehchoice _ _) as [gt | eq]. { contradiction (isirreflnatlth _ gt). } apply (@nonzeroax F). - apply funextfun; intros j. destruct (natlthorgeh j zero) as [? | ge]. + rewrite back_sub_internal_inv2; try easy. * apply dualelement_sn_stn_ge_n. * now apply (pr2 iszero). + rewrite matrix_mult_eq; unfold matrix_mult_unf. unfold col_vec, const_vec. apply funextfun; intros ?. eapply (@vecsum_eq_zero F). intros k. destruct (natgthorleh j k) as [? | le]. { rewrite ut; try assumption; apply rigmult0x. } destruct (stn_eq_or_neq (zero) k) as [eq | ?]. * rewrite <- eq in *. rewrite <- (stn_eq _ _ (isantisymmnatgeh _ _ le ge)). rewrite (pr1 iszero); apply rigmult0x. * etrans. 2: { apply rigmultx0. } apply maponpaths. rewrite back_sub_internal_inv1; try assumption. 2: { apply (istransnatleh ge le). } destruct (natlthorgeh _ _) as [? | ?]; try reflexivity. destruct (natgehchoice _ _) as [? | eq]; try reflexivity. rewrite (stn_eq _ _ eq) in * |-. contradiction (isirrefl_natneq k). 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