proposition: Lemma pos_expr_if_all_pos : forall pe1 pe2, all_coef_pos ( norm_subst 0 1 Zplus Zmult Zminus Z.opp Zeq_bool Z.div_eucl ring_subst_niter nil (PEsub pe2 pe1) ) = true -> forall l, all_mem_pos l -> PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower l pe1 <= PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower l pe2 .
proof: Proof. intros pe1 pe2 H l H0. assert (0<= PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower l (PEsub pe2 pe1)). apply pos_expr_if_all_pos'. assumption. assumption. simpl in H1;auto with zarith. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)