proposition: Lemma eval_some_notInf : forall n (mi : mint n) (v : vector dom n), Vexists (fun m => get_elem m dim_pos dim_pos <> MinusInf) (args mi) -> Vfold_left_rev Aplus A0 (Vmap (fun v => Vnth v dim_pos) (Vmap2 mat_times_vec (args mi) (Vmap dom2vec v))) <> MinusInf.
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 arctic_plus_notInf_left. apply mat_times_vec_at0_positive. hyp. VSntac v. simpl. destruct (Vhead v). unfold vec_invariant, Conf.vec_at0 in v0. simpl in *. apply ge_A1_not_minusInf. hyp. apply arctic_plus_notInf_left. rewrite <- Vmap_tail. apply (IHn (mkMatrixInt const (Vtail args))). hyp. Qed.
imports: CoLoR(AArcticBasedInt Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil NatUtil AWFMInterpretation LogicUtil AMatrixBasedInt BoolUtil ListUtil)