proposition: Lemma pmonotone_imp_pmonotone' : forall n (p : poly n), pstrong_monotone p -> pstrong_monotone' p.
proof: Proof. intros n p (H1, H2). split. auto. intros i Hi. gen (H2 i Hi). clear H2. generalize dependent p. intro p. elim p. intros H1 H2. absurd (coef (mxi Hi) nil = 0). lia. simpl. refl. intros (c, m) p' Hrec H1. simpl in H1. gen H1. clear H1. intros (H1, H2). simpl. case (monom_eq_dec (mxi Hi) m); intro Hm; simpl. elim (Z_le_lt_eq_dec _ _ H1); clear H1. intro H1. intro H'. exists (pzero n). exists c. exists p'. split. hyp. simpl. subst m. refl. intro Hc. subst c. subst m. simpl. intro H3. elim (Hrec H2 H3). clear Hrec. intros p'1 H. elim H. clear H. intros c' H. elim H. clear H. intros p'2 (Hc', Hp'). exists ((0, mxi Hi) :: p'1). exists c'. exists p'2. split. hyp. rewrite Hp'. refl. intro H3. elim (Hrec H2 H3). clear H2. clear H3. intros p'1 H. elim H. clear H. intros c' H. elim H. clear H. intros p'2 (Hc', Hp'). exists ((c, m) :: p'1). exists c'. exists p'2. split. hyp. subst p'. simpl. refl. Qed.
imports: CoLoR(Polynom PositivePolynom NaryFunction VecUtil LogicUtil ListUtil ZUtil RelUtil NatUtil BoundNat)