proposition: Lemma pos_pol_incr' : forall (p:Pol Z), all_coef_pos p = true -> forall l1 l2, all_le l1 l2 -> all_mem_pos l1 -> 0<=@Pphi_pow _ 0 1 Zplus Zmult Zminus Z.opp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_signZ) l1 p <= @Pphi_pow _ 0 1 Zplus Zmult Zminus Z.opp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_signZ) l2 p.
proof: Proof. intros p H l1 l2 H0 H1. replace (@Pphi_pow _ 0 1 Zplus Zmult Zminus Z.opp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_signZ) l1 p) with (Pphi 0 Zplus Zmult (@IDphi Z) l1 p). replace (Pphi_pow 0 1 Zplus Zmult Zminus Z.opp 0 1 Zeq_bool (IDphi (R:=Z)) Z_of_N Zpower (get_signZ) l2 p) with (Pphi 0 Zplus Zmult (@IDphi Z) l2 p). apply pos_pol_incr;assumption. symmetry;eapply Pphi_pow_ok with (1:=InitialRing.Zsth) (C:= Z). exact InitialRing.Zeqe. exact (@Rth_ARth _ _ _ _ _ _ _ _ InitialRing.Zsth InitialRing.Zeqe InitialRing.Zth). eexact (@IDmorph Z Z0 1 Zplus Zmult Zminus Z.opp _ InitialRing.Zsth Zeq_bool Zeq_bool_eq). exact Zpower_theory. apply get_signZ_th. symmetry;eapply Pphi_pow_ok with (1:=InitialRing.Zsth) (C:= Z). exact InitialRing.Zeqe. exact (@Rth_ARth _ _ _ _ _ _ _ _ InitialRing.Zsth InitialRing.Zeqe InitialRing.Zth). eexact (@IDmorph Z Z0 1 Zplus Zmult Zminus Z.opp _ InitialRing.Zsth Zeq_bool Zeq_bool_eq). exact Zpower_theory. apply get_signZ_th. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)