proposition: Lemma mat_times_vec_at0_positive n (m : matrix n n) (v : vector A n) (dim_pos : n > 0) : get_elem m dim_pos dim_pos <> PlusInf -> Vnth v dim_pos <> PlusInf -> Vnth (mat_vec_prod m v) dim_pos <> PlusInf.
proof: Proof. destruct n; intros. lia. VSntac v. unfold matrix in m. VSntac m. unfold mat_vec_prod, col_mat_to_vec, get_col. rewrite Vnth_map. set (w := mat_mult_spec). unfold get_elem, get_row in w. rewrite w. simpl. VSntac (Vhead m). unfold dot_product. simpl. rewrite Aplus_comm. apply tropical_plus_notInf_left. apply tropical_mult_notInf. rewrite H2 in H. unfold get_elem in H. simpl in H. rewrite Vhead_nth, <- (Vnth_eq (Vhead m) dim_pos (PeanoNat.Nat.lt_0_succ n)); trivial. rewrite H1 in H0. hyp. Qed.
imports: CoLoR(ATropicalBasedInt Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil NatUtil AWFMInterpretation LogicUtil AMatrixBasedInt BoolUtil ListUtil) Coq(Structures.Equalities)