proposition: Lemma pmonotone'_imp_monotone_peval_Dlt : forall n (p : poly n) (H: pstrong_monotone' p), Vmonotone1 (peval_D (proj1 H)) Dlt.
proof: Proof. intros n p (H_coef_pos_p, H_pmonotone_p) i j Hij. gen (H_pmonotone_p _ (i_lt_n (sym_equal Hij))). intro H. elim H. clear H. intros p1 H. elim H. clear H. intros c H. elim H. clear H. intros p2 (H, H'). subst p. gen (coef_pos_app H_coef_pos_p). intros (H_coef_pos_p1, H'). gen (coef_pos_cons H'). clear H'. intros (H', H_coef_pos_p2). clear H'. unfold Vmonotone_i, Dlt, peval_D. unfold monotone, restrict. intros vi vj. destruct x as (x, Hx). destruct y as (y, Hy). simpl. intro Hxy. clear H_coef_pos_p. rewrite !peval_app. apply Zplus_le_lt_compat. gen (coef_pos_monotone_peval_Dle H_coef_pos_p1). unfold Vmonotone, Dle, peval_D. unfold Vmonotone_i, restrict. unfold monotone. intro H'. gen (H' _ _ Hij vi vj (exist Hx) (exist Hy)). simpl. clear H'. intro H'. apply H'. lia. lazy beta iota delta [peval]. fold peval. apply Zplus_lt_le_compat. apply Zmult_lt_compat_l. hyp. rewrite !meval_xi, !Vmap_cast. case Hij. simpl. clear H_pmonotone_p. clear Hij. generalize dependent i. intro i. elim i. intro vi. rewrite (VO_eq vi). simpl. hyp. intros i' Hrec vi. rewrite (VSn_eq vi). simpl Vapp. simpl Vmap. simpl Vnth. gen (Hrec (Vtail vi)). clear Hrec. intro H'. assert (H'' : i_lt_n (eq_refl (i' + S j)%nat) = NatCompat.lt_S_n (@i_lt_n (S (i' + S j)) (S i') _ (eq_refl (S (i' + S j))))). apply lt_unique. rewrite <- H''. hyp. gen (coef_pos_monotone_peval_Dle H_coef_pos_p2). unfold Vmonotone, Dle, peval_D. unfold Vmonotone_i, restrict. unfold monotone. intro H'. gen (H' _ _ Hij vi vj (exist Hx) (exist Hy)). simpl. clear H'. intro H'. apply H'. lia. Qed.
imports: CoLoR(Polynom PositivePolynom NaryFunction VecUtil LogicUtil ListUtil ZUtil RelUtil NatUtil BoundNat)