proposition: Lemma pos_expr_if_all_pos' : forall pe, all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Z.opp Zeq_bool Z.div_eucl ring_subst_niter nil pe) = true -> forall l, all_mem_pos l -> 0<= (PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower l pe) .
proof: Proof. intros p H l H0. rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z)) (l:=l) (lmp:=@nil (Z*Mon * Pol Z)) (pe:=p) (npe:= norm_subst 0 1 Zplus Zmult Zminus Z.opp Zeq_bool Z.div_eucl ring_subst_niter nil p). apply pos_expr_if_all_pos_aux';assumption. vm_compute;exact I. vm_compute;reflexivity. reflexivity. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)