proposition: Lemma vec_add_monotone_map2 : forall n1 (v1 : vector vec n1) n2 (v2 : vector vec n2) n (M : vector (matrix dim dim) n) i_j, Vforall (fun m => get_elem m dim_pos dim_pos > 0) M -> a >=v b -> vec_at0 a > vec_at0 b -> vec_at0 (add_vectors (Vmap2 f M (Vcast (Vapp v1 (Vcons a v2)) i_j))) > vec_at0 (add_vectors (Vmap2 f M (Vcast (Vapp v1 (Vcons b v2)) i_j))).
proof: Proof. induction v1; intros; simpl. destruct n. lia. rewrite !Vcast_cons. unfold add_vectors, MBI.vec_at0, vector_plus. simpl. rewrite !Vnth_map2. unfold Aplus. apply plus_gt_compat_r. apply eq_ge_compat. refl. unfold MBI.vec_at0 in f_mon. apply f_mon; try hyp. apply (Vforall_in (x:=Vhead M) H). apply Vin_head. destruct n0. lia. rewrite !Vcast_cons. unfold add_vectors, MBI.vec_at0, vector_plus. simpl. rewrite !Vnth_map2. unfold Aplus. apply plus_gt_compat_l. 2: apply eq_ge_compat; refl. match goal with |- gt ?Hl ?Hr => fold (gt Hr Hl) end. unfold MBI.vec_at0, add_vectors in IHv1. apply IHv1; try hyp. apply Vforall_incl with (S n0) M. intros. VSntac M. simpl. auto. hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil BigNUtil AMatrixBasedInt)