proposition: Lemma pmonotone_imp_monotone_peval_Dlt : forall n (p : poly n) (wm : pweak_monotone p) (sm : pstrong_monotone p), Vmonotone1 (peval_D wm) Dlt.
proof: Proof. intros n p wm sm. gen (pmonotone'_imp_monotone_peval_Dlt (pmonotone_imp_pmonotone' sm)). unfold Vmonotone1, Vmonotone, Dlt, Vmonotone_i, peval_D, restrict, monotone. intros H0 i j Hij vi vj. destruct x as (x, Hx). destruct y as (y, Hy). simpl. intro Hxy. gen (H0 i j Hij vi vj (exist Hx) (exist Hy) Hxy). clear H0. simpl. intuition. Qed.
imports: CoLoR(Polynom PositivePolynom NaryFunction VecUtil LogicUtil ListUtil ZUtil RelUtil NatUtil BoundNat)