proposition: Lemma bpstrong_monotone_ok : forall n (p : poly n), bpstrong_monotone p = true <-> pstrong_monotone p.
proof: Proof. induction p. unfold pstrong_monotone, bpstrong_monotone, pweak_monotone. simpl. intuition. unfold L in H. destruct n. lia. destruct n; discr. destruct n. refl. ded (H1 n (le_n (S n))). lia. destruct a. intuition. unfold pstrong_monotone, pweak_monotone. unfold bpstrong_monotone, bcoef_pos in H1. Opaque coef. simpl in *. rewrite !andb_eq in H1. intuition. change (bcoef_pos p = true) in H4. rewrite <- is_not_neg_ok. hyp. rewrite <- bcoef_pos_ok. hyp. assert (In (N_ H2) (L n)). apply In_L. rewrite forallb_forall in H3. ded (H3 _ H5). rewrite is_pos_ok in H6. simpl in H6. lia. unfold pstrong_monotone, pweak_monotone in H1. unfold bpstrong_monotone, bcoef_pos. simpl in *. rewrite !andb_eq. intuition. rewrite is_not_neg_ok. hyp. change (bcoef_pos p = true). rewrite bcoef_pos_ok. hyp. rewrite forallb_forall. intros [i hi]. simpl. rewrite is_pos_ok. ded (H3 _ hi). lia. Transparent coef. Qed.
imports: CoLoR(Polynom PositivePolynom NaryFunction VecUtil LogicUtil ListUtil ZUtil RelUtil NatUtil BoundNat) CoLoR(BoolUtil)