proposition: Lemma vec_add_weak_monotone_map2 : forall n1 (v1 : vector vec n1) n2 (v2 : vector vec n2) n (M : vector (matrix dim dim) n) i_j, a >=v b -> add_vectors (Vmap2 f M (Vcast (Vapp v1 (Vcons a v2)) i_j)) >=v add_vectors (Vmap2 f M (Vcast (Vapp v1 (Vcons b v2)) i_j)).
proof: Proof. induction v1; intros; simpl. destruct n; try solve [lia]. rewrite !Vcast_cons. simpl. unfold add_vectors, succeq. simpl. apply Vforall2_intro_nth. intros. unfold vector_plus. rewrite !Vnth_map2. assert (Vnth (f (Vhead M) a) ip >>= Vnth (f (Vhead M) b) ip). apply Vforall2_elim_nth. apply f_mon. hyp. apply plus_ge_compat. apply ge_refl. hyp. destruct n0; try solve [lia]. rewrite !Vcast_cons. simpl. unfold add_vectors, succeq. simpl. apply Vforall2_intro_nth. intros. unfold vector_plus. rewrite !Vnth_map2. apply plus_ge_compat. apply Vforall2_elim_nth. unfold add_vectors in IHv1. apply IHv1. hyp. apply ge_refl. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)