proposition: Lemma pos_expr_incr_aux : 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 l1 l2, all_le l1 l2 -> all_mem_pos l1 -> 0 <= PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower l1 pe <= ( PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower l2 pe) .
proof: Proof. intros pe H l1 l2 H0 H1. 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 pos_pol_incr';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)