proposition: Lemma meval_monotone_D : forall i (vi : vec i) (mi : monom i) j (vj : vec j) (mj : monom j) k x y (Hx : 0 <= x) (Hy : 0 <= y), x<=y -> meval (Vapp mi (Vcons k mj)) (vals (Vapp vi (Vcons (inj Hx) vj))) <= meval (Vapp mi (Vcons k mj)) (vals (Vapp vi (Vcons (inj Hy) vj))).
proof: Proof. intros. rewrite !Vmap_app. simpl Vmap. rewrite !meval_app. apply Zmult_le_compat_l. simpl meval. apply Zmult_le_compat_r. apply power_le_compat; hyp. apply pos_meval. apply pos_meval. Qed.
imports: CoLoR(Polynom PositivePolynom NaryFunction VecUtil LogicUtil ListUtil ZUtil RelUtil NatUtil BoundNat)