proposition: Lemma back_sub_step_inv0 { n : nat } (row : ⟦ n ⟧%stn) (mat : Matrix F n n) (x : Vector F n) (b : Vector F n) (p: @is_upper_triangular F n n mat) (p' : (mat row row != 0)%ring) : (mat ** (col_vec (back_sub_step row mat x b))) row = (col_vec b) row.
proof: Proof. unfold back_sub_step, col_vec. unfold fldmultinv'. rewrite matrix_mult_eq; unfold matrix_mult_unf, pointwise. set (m := n - (S row)). assert (split_eq : n = (S row) + m). { unfold m. rewrite natpluscomm, minusplusnmm. - apply idpath. - exact (pr2 row). } destruct (stn_inhabited_implies_succ row) as [s_row s_row_eq], (!s_row_eq). apply funextfun; intros ?. rewrite (@vecsum_dni _ (s_row) _ row) , nat_eq_or_neq_refl. destruct (fldchoice0 _) as [? | neq]. { contradiction. } etrans. { apply maponpaths_2; apply maponpaths. apply funextfun; intros q. unfold funcomp. now rewrite (nat_eq_or_neq_right (dni_neq_i row q)). } rewrite (@vecsum_dni F (s_row) _ row). etrans. { apply maponpaths. etrans. { apply maponpaths. rewrite (@ringcomm2 F). apply maponpaths. now rewrite (@ringcomm2 F). } apply (@ringminusdistr' F (mat row row)). } etrans. { apply maponpaths; apply map_on_two_paths. - rewrite <- (@rigassoc2 F), (@fldmultinvrax F). { now rewrite (@riglunax2 F). } - apply maponpaths. rewrite <- (@rigassoc2 F), (@fldmultinvrax F). apply (@riglunax2 F). } etrans. { do 3 apply maponpaths. now rewrite (@rigcomm2 F), (@ringplusminus F). } rewrite (@rigcomm1 F); rewrite (@rigassoc1 F). now rewrite (@ringlinvax1 F), (@rigrunax1 F). 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