proposition: Lemma coef_pos_monotone_peval_Dle : forall n (p : poly n) (H : coef_pos p), Vmonotone1 (peval_D H) Dle.
proof: Proof. unfold Vmonotone1, Vmonotone, Dle, peval_D, Vmonotone_i, restrict, monotone. intros n p H_coef_pos i j Hij vi vj. destruct x as (x, Hx). destruct y as (y, Hy). simpl. intro Hxy. generalize dependent p. intro p. elim p. intro. simpl. lia. unfold coef_pos. intros (c, m) p' Hrec H_coef_pos. simpl in H_coef_pos. gen H_coef_pos. clear H_coef_pos. intros (H_pos_c, H_coef_pos_p'). gen (Hrec H_coef_pos_p'). clear Hrec. clear H_coef_pos_p'. intro H. lazy beta iota delta [peval]. fold peval. apply Zplus_le_compat. 2: apply H. clear H. apply Zmult_le_compat_l. 2: hyp. rewrite (Vbreak_eq_app_cast Hij m). set (mi := (fst (Vbreak (n1:=i) (n2:=S j) (Vcast m (sym_equal Hij))))). set (mj := (snd (Vbreak (n1:=i) (n2:=S j) (Vcast m (sym_equal Hij))))). rewrite (VSn_eq mj). case Hij. simpl. apply meval_monotone_D. hyp. Qed.
imports: CoLoR(Polynom PositivePolynom NaryFunction VecUtil LogicUtil ListUtil ZUtil RelUtil NatUtil BoundNat)