proposition: Lemma strict_pos_expr_if_all_pos_aux : forall (p:Pol Z), all_coef_pos p = true -> forall lb, all_mem_pos lb -> forall lz, length lb = length lz -> all_mem_bounded (combine lb lz) -> 0 < Pphi 0 Zplus Zmult (IDphi (R:=Z)) lb p -> 0< Pphi 0 Zplus Zmult (IDphi (R:=Z)) lz p.
proof: Proof. induction p. intros H lb H0 lz H1 H2 H3;tauto. simpl. intros Hp0 lb lb_pos lz Hlength lb_lz H. apply IHp with (jump p lb);try assumption. apply all_mem_pos_jump;exact lb_pos. apply jump_length;exact Hlength. rewrite combine_jump;apply all_mem_bounded_jump;exact lb_lz. simpl. intros Hp1_p3 lb lb_pos lz Hlength lb_lz H. assert(h1:0<=pow_pos Zmult (hd 0 lb) p2). destruct lb. simpl; clear; induction p2; simpl; auto with zarith. simpl. simpl in lb_pos. destruct lb_pos. clear - H0. induction p2; simpl; auto with zarith. assert (h2:0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) lb p1). apply pos_expr_if_all_pos_aux. symmetry in Hp1_p3;destruct (@andb_true_eq _ _ Hp1_p3);auto. exact lb_pos. assert (h3:0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) lb p1 * pow_pos Zmult (hd 0 lb) p2). auto with zarith. assert(h4:(0<Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail lb) p3)\/0<Pphi 0 Zplus Zmult (IDphi (R:=Z)) lb p1 * pow_pos Zmult (hd 0 lb) p2). case(Zle_lt_or_eq _ _ h3). auto. intro Heq;rewrite <- Heq in H;simpl in H;auto. assert(h5:0<=pow_pos Zmult (hd 0 lz) p2). destruct lz. simpl; clear; induction p2; simpl; auto with zarith. simpl. destruct lb;try discriminate. simpl in lb_pos. destruct lb_pos. simpl in lb_lz;destruct lb_lz. assert (0<= z) by auto with zarith. clear - H4. induction p2; simpl; auto with zarith. assert (h6:0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) lz p1). apply pos_expr_if_all_pos_aux. symmetry in Hp1_p3;destruct (@andb_true_eq _ _ Hp1_p3);auto. apply all_mem_pos_all_mem_bounded with lb. exact Hlength. exact lb_pos. exact lb_lz. assert (h7:0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) lz p1 * pow_pos Zmult (hd 0 lz) p2). auto with zarith. case h4;clear h4;intro h4. assert (h8:0< Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail lz) p3). apply IHp2 with (tail lb). symmetry in Hp1_p3;destruct (@andb_true_eq _ _ Hp1_p3);auto. apply all_mem_pos_tail;exact lb_pos. apply tail_length;exact Hlength. rewrite combine_tail;apply all_mem_bounded_tail;exact lb_lz. exact h4. auto with zarith. destruct (Zmult_compat _ _ h2 h4) as [h8 h9];clear h4. assert (h10:0 < Pphi 0 Zplus Zmult (IDphi (R:=Z)) lz p1). apply IHp1 with lb. symmetry in Hp1_p3;destruct (@andb_true_eq _ _ Hp1_p3);auto. exact lb_pos. exact Hlength. exact lb_lz. exact h8. assert (h11: 0 < pow_pos Zmult (hd 0 lz) p2). destruct lz. clear - h9 Hlength lb_lz. destruct lb;try discriminate. simpl in h9|-*. clear - h9; apply False_ind. replace (pow_pos Zmult 0 p2) with 0 in *. lia. clear. induction p2;simpl. 1, 3: reflexivity. rewrite <- IHp2;ring. simpl. clear - h9 Hlength lb_pos lb_lz. destruct lb;try discriminate. simpl in h9,lb_lz,lb_pos|-*. destruct lb_lz as [h _]. destruct lb_pos as [h1 _]. clear - h h1 h9. apply Z.lt_le_trans with (pow_pos Zmult z0 p2). assumption. apply pow_pos_monotonic;auto with zarith. assert (0 < Pphi 0 Zplus Zmult (IDphi (R:=Z)) lz p1 * pow_pos Zmult (hd 0 lz) p2). apply Zmult_lt_0_compat;assumption. assert ( 0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail lz) p3). apply pos_expr_if_all_pos_aux. symmetry in Hp1_p3;destruct (@andb_true_eq _ _ Hp1_p3);auto. apply all_mem_pos_tail. apply all_mem_pos_all_mem_bounded with lb; assumption. lia. Defined.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)