proposition: Lemma eval_some_notInf : forall n (mi : mint n) (v : vector dom n), Vexists (fun m => get_elem m dim_pos dim_pos <> PlusInf) (args mi) -> Vfold_left_rev Aplus A0 (Vmap (fun v => Vnth v dim_pos) (Vmap2 mat_times_vec (args mi) (Vmap dom2vec v))) <> PlusInf.
proof: Proof. induction n; intros; simpl; destruct mi. VOtac. auto. simpl in H. VSntac args. rewrite H0 in H; simpl. destruct H. rewrite Aplus_comm. apply tropical_plus_notInf_left. apply (@mat_times_vec_at0_positive dim). hyp. VSntac v. simpl. destruct (Vhead v). unfold vec_invariant, Conf.vec_at0 in v0. simpl in *. intuition. clear H1. rewrite H2 in v0. contr. apply tropical_plus_notInf_left. rewrite <- Vmap_tail. apply (IHn (mkMatrixInt const (Vtail args))). hyp. Qed.
imports: CoLoR(ATropicalBasedInt Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil NatUtil AWFMInterpretation LogicUtil AMatrixBasedInt BoolUtil ListUtil) Coq(Structures.Equalities)