proposition: Lemma pos_expr_if_all_pos_aux : forall (p:Pol Z), all_coef_pos p = true -> forall l, all_mem_pos l -> 0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p.
proof: Proof. intros p;functional induction (all_coef_pos p). intro;discriminate. intros _. simpl. destruct c;simpl in y;try discriminate;simpl;auto with zarith. unfold IDphi;auto with zarith. simpl. intros H l H0. apply IHb. exact H. rewrite <- all_mem_pos_def in H0|-*. intros c H1. apply H0. apply jump_in with _x;exact H1. simpl. intros H l H0. assert (0<=hd 0 l). clear - H0. induction l. simpl;lia. simpl. rewrite <- all_mem_pos_def in H0;simpl in H0;eauto. assert (0<= pow_pos Zmult (hd 0 l) _x). set (u:=hd 0 l) in *;clearbody u. clear - H1. induction _x. simpl; auto with zarith. simpl; auto with zarith. simpl; auto with zarith. assert (0 <= Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p0). apply IHb. symmetry in H. destruct (@andb_true_eq _ _ H);auto. assumption. assert (0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l) q). apply IHb0. symmetry in H;destruct (@andb_true_eq _ _ H);auto. rewrite <- all_mem_pos_def in H0|-*. intros c H4; apply H0;apply tail_in;exact H4. auto with zarith. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)