proposition: Lemma strict_pos_expr_if_all_pos_aux' : forall (p:Pol Z), all_coef_pos p = true -> forall lb, all_mem_pos lb -> forall lz, length lb = length lz -> all_mem_bounded (combine lb lz) -> 0< @Pphi_pow _ 0 1 Zplus Zmult Zminus Z.opp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_signZ) lb p -> 0< @Pphi_pow _ 0 1 Zplus Zmult Zminus Z.opp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_signZ) lz p.
proof: Proof. intros p H lb H0 lz H1 H2. replace ( @Pphi_pow _ 0 1 Zplus Zmult Zminus Z.opp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_signZ) lb p) with (Pphi 0 Zplus Zmult (@IDphi Z) lb p). replace (Pphi_pow 0 1 Zplus Zmult Zminus Z.opp 0 1 Zeq_bool (IDphi (R:=Z)) Z_of_N Zpower (get_signZ) lz p) with (Pphi 0 Zplus Zmult (@IDphi Z) lz p). intro. apply strict_pos_expr_if_all_pos_aux with lb;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)