proposition: Lemma mi_eval_at0 : forall n (mi : matrixInt dim n) (v : vector dom n), somewhere_finite dim_pos mi -> vec_at0 (mi_eval_aux mi (Vmap dom2vec v)) <> MinusInf.
proof: Proof. intros. unfold mi_eval_aux, vec_at0. rewrite vector_plus_nth. destruct H. rewrite add_vectors_nth. apply arctic_plus_notInf_left. apply eval_some_notInf. hyp. rewrite Aplus_comm. apply arctic_plus_notInf_left. hyp. Qed.
imports: CoLoR(AArcticBasedInt Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil NatUtil AWFMInterpretation LogicUtil AMatrixBasedInt BoolUtil ListUtil)