proposition: Lemma strict_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 lb, all_mem_pos lb -> forall lz, length lb = length lz -> all_mem_bounded (combine lb lz) -> 0 < PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lb pe -> 0< ( PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lz pe) .
proof: Proof. intros pe H lb lb_pos lz Hlength Hlb_lz. rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z)) (lmp:=@nil (Z*Mon * Pol Z)) (pe:=pe) (npe:=norm_subst 0 1 Zplus Zmult Zminus Z.opp Zeq_bool Z.div_eucl ring_subst_niter nil pe). rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z)) (lmp:=@nil (Z*Mon * Pol Z)) (pe:=pe) (npe:=norm_subst 0 1 Zplus Zmult Zminus Z.opp Zeq_bool Z.div_eucl ring_subst_niter nil pe). apply strict_pos_expr_if_all_pos_aux';assumption. vm_compute;exact I. vm_compute;reflexivity. reflexivity. vm_compute;exact I. vm_compute;reflexivity. reflexivity. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)