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 0 Zplus Zmult (IDphi (R:=Z)) l1 p <= Pphi 0 Zplus Zmult (IDphi (R:=Z)) l2 p.
proof: Proof. intros p;functional induction (all_coef_pos p). intro;discriminate. intros _. simpl. destruct c;simpl in y;try discriminate;simpl;split;unfold IDphi;auto with zarith. simpl. intros H l1 l2 H0 H1. apply IHb. exact H. rewrite all_le_def in H0|-*. destruct H0 as [Hlength Hforall]. split. apply jump_length;exact Hlength. intros x y H0;apply Hforall;apply jump_in with _x. rewrite jump_combine;assumption. rewrite <- all_mem_pos_def in H1|-*. intros c H2;apply H1;apply jump_in with _x;assumption. simpl. intros H l1 l2 H0 H1. assert (0<=pow_pos Zmult (hd 0 l1) _x <= pow_pos Zmult (hd 0 l2) _x). destruct l1;destruct l2;simpl in H0;try tauto;simpl;auto with zarith. clear;induction _x;simpl;auto with zarith. destruct H0. simpl in H1;destruct H1 as [ H1 _ ]. clear - H0 H1. assert (0<=z0);auto with zarith. generalize dependent z0;generalize dependent z. induction _x;simpl;intros. assert (0<=pow_pos Zmult z _x) by (clear -H1;induction _x;simpl;auto with zarith). assert (z*pow_pos Zmult z _x <= z0 * pow_pos Zmult z0 _x). destruct (IH_x _ H1 _ H0 H);apply Z.le_trans with (z0*pow_pos Zmult z _x); auto with zarith. split. auto with zarith. destruct (IH_x _ H1 _ H0 H). do 2 rewrite Zmult_assoc. apply Z.le_trans with (z*pow_pos Zmult z _x * pow_pos Zmult z0 _x);auto with zarith. destruct (IH_x _ H1 _ H0 H). split;auto with zarith. assert (0<= pow_pos Zmult z0 _x). apply Z.le_trans with (pow_pos Zmult z _x);auto with zarith. apply Z.le_trans with (pow_pos Zmult z _x*pow_pos Zmult z0 _x);auto with zarith. auto with zarith. assert (0 <= Pphi 0 Zplus Zmult (IDphi (R:=Z)) l1 p0 <= Pphi 0 Zplus Zmult (IDphi (R:=Z)) l2 p0). apply IHb. symmetry in H. destruct (@andb_true_eq _ _ H);auto. assumption. assumption. assert (0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l1) q <= Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l2) q). apply IHb0. symmetry in H;destruct (@andb_true_eq _ _ H);auto. destruct l1;destruct l2;simpl in H0;simpl;auto;try tauto. rewrite <- all_mem_pos_def in H1|-*. intros c H4; apply H1;apply tail_in;exact H4. destruct H2;destruct H3;destruct H4;split;auto with zarith. assert (0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) l2 p0) by (apply Z.le_trans with (Pphi 0 Zplus Zmult (IDphi (R:=Z)) l1 p0);auto with zarith). assert (0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l2) q) by (apply Z.le_trans with (Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l1) q);auto with zarith). assert (0 <= pow_pos Zmult (hd 0 l2) _x) by (apply Z.le_trans with (pow_pos Zmult (hd 0 l1) _x);auto with zarith). assert (Pphi 0 Zplus Zmult (IDphi (R:=Z)) l1 p0 * pow_pos Zmult (hd 0 l1) _x <= Pphi 0 Zplus Zmult (IDphi (R:=Z)) l2 p0 * pow_pos Zmult (hd 0 l2) _x) by (apply Z.le_trans with (Pphi 0 Zplus Zmult (IDphi (R:=Z)) l2 p0 * pow_pos Zmult (hd 0 l1) _x);auto with zarith). auto with zarith. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)