proposition: Lemma strict_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 lb, all_mem_pos lb -> forall lz, length lb = length lz -> all_mem_bounded (combine lb lz) -> PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lb pe1 < PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lb pe2 -> PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lz pe1 < ( PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lz pe2) .
proof: Proof. intros pe1 pe2 H lb H0 lz H1 H2 H3. assert (0< PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lz pe2 - PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lz pe1). replace (PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lz pe2 - PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lz pe1) with (PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lz (PEsub pe2 pe1)) by (vm_compute;reflexivity). apply strict_pos_expr_if_all_pos' with lb. assumption. assumption. assumption. assumption. simpl. auto with zarith. auto with zarith. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)