proposition: Lemma mi_eval_at0 : forall n (mi : matrixInt dim n) (v : vector dom n), absolute_finite dim_pos mi -> vec_at0 (mi_eval_aux mi (Vmap dom2vec v)) >>= A1.
proof: Proof. intros. unfold mi_eval_aux, vec_at0. rewrite vector_plus_nth, Aplus_comm. apply arctic_plus_ge_monotone. exact H. Qed.
imports: Coq(ZArith Lia) CoLoR(LogicUtil Matrix AMonAlg AArcticBasedInt VecUtil OrdSemiRing SN RelUtil AMatrixBasedInt ListUtil)