# Library examples.cime_trace.ring_extention

``` Require Import ZArith. Require Import ZArithRing. Require Import Ring_polynom. Require Import Bool. Require Import List. Function all_coef_pos (p:Pol Z) : bool :=   match p with     | Pc c => match Zcompare 0 c with                 | Gt => false                 | _ => true               end     | Pinj _ p => all_coef_pos p     | PX p _ q => andb (all_coef_pos p) (all_coef_pos q)   end. Function all_mem_pos (l:list Z) : Prop :=   match l with     | nil => True     | c::l => (0<=c)%Z /\ all_mem_pos l   end. Open Scope Z_scope. Import InitialRing. Import BinList. Functional Scheme jump_ind := Induction for jump Sort Prop. Open Scope Z_scope. Lemma all_mem_pos_def : forall l, (forall c, In c l -> 0<= c) <-> all_mem_pos l. Proof. intro l;split;intro H. induction l. simpl. trivial. simpl. split. apply H;simpl;auto. apply IHl;intro;simpl in H;auto. functional induction (all_mem_pos l). simpl;tauto. destruct H;simpl. intros x H';simpl in H';destruct H'. subst. assumption. auto. Qed. Lemma tail_in : forall A (l:list A) x, In x (tail l) -> In x l. Proof.   induction l.   simpl;tauto.   simpl.   auto. Qed. Lemma jump_in : forall A n l (x:A), In x (jump n l) -> @In A x l. Proof. intros a n l;functional induction (jump n l). intros;apply tail_in;eauto. eauto. intros;apply tail_in;auto. Qed. Lemma pos_expr_if_all_pos_aux :   forall (p:Pol Z), all_coef_pos p = true -> forall l, all_mem_pos l ->     0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p. Proof.   intros p;functional induction (all_coef_pos p).   intro;discriminate.   intros _.   simpl.   destruct c;simpl in y;try discriminate;simpl;auto with zarith.   unfold IDphi;auto with zarith.   simpl.   intros H l H0.   apply IHb.   exact H.   rewrite <- all_mem_pos_def in H0|-*.   intros c H1.   apply H0.   apply jump_in with _x;exact H1.   simpl.   intros H l H0.   assert (0<=hd 0 l).   clear - H0.   induction l.   simpl;omega.   simpl.   rewrite <- all_mem_pos_def in H0;simpl in H0;eauto.   assert (0<= pow_pos Zmult (hd 0 l) _x).   set (u:=hd 0 l) in *;clearbody u.   clear - H1.   induction _x.   simpl; auto with zarith.   simpl; auto with zarith.   simpl; auto with zarith. assert (0 <=    Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p0). apply IHb. symmetry in H. destruct (@andb_true_eq _ _ H);auto. assumption. assert (0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l) q). apply IHb0. symmetry in H;destruct (@andb_true_eq _ _ H);auto. rewrite <- all_mem_pos_def in H0|-*.   intros c H4; apply H0;apply tail_in;exact H4. auto with zarith. Qed. Lemma pos_expr_if_all_pos_aux' :   forall (p:Pol Z), all_coef_pos p = true -> forall l, all_mem_pos l ->     0<=     @Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l p. Proof.   intros p H l H0.   replace ( @Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l p)     with (Pphi 0 Zplus Zmult (@IDphi Z) l p).   apply pos_expr_if_all_pos_aux;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 Zopp _ InitialRing.Zsth Zeq_bool InitialRing.Zeqb_ok).   exact Zpower_theory.   constructor.   destruct c;simpl;try (intros;discriminate). Qed. Lemma pos_expr_if_all_pos' :   forall pe,     all_coef_pos     (norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil pe) = true ->     forall l, all_mem_pos l ->     0<= ( PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe) . Proof.   intros p H l H0.   rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z)) (l:=l)     (lmp:=@nil (Mon * Pol Z)) (pe:=p) (npe:=norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil            p).   apply pos_expr_if_all_pos_aux';assumption.   vm_compute;exact I.   vm_compute;reflexivity.   reflexivity. Qed. Lemma pos_expr_if_all_pos :   forall pe1 pe2,     all_coef_pos ( norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil (PEsub pe2 pe1)) = true ->     forall l, all_mem_pos l ->       PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe1 <=     PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe2 . Proof.   intros pe1 pe2 H l H0.   assert (0<= PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l (PEsub pe2 pe1)).   apply pos_expr_if_all_pos'.   assumption.   assumption.   simpl in H1;auto with zarith. Qed. Lemma jump_nil : forall p, jump p (@nil Z) = nil . Proof.   induction p;simpl.   do 2 rewrite IHp;reflexivity.   do 2 rewrite IHp;reflexivity.   reflexivity. Qed. Lemma Pphi_nil : forall p,   Pphi 0 Zplus Zmult (IDphi (R:=Z)) nil p =   match p with     | Pc c => c     | Pinj _ p => Pphi 0 Zplus Zmult (IDphi (R:=Z)) nil p     | PX _ _ p => Pphi 0 Zplus Zmult (IDphi (R:=Z)) nil p   end. Proof. destruct p. simpl;unfold IDphi;reflexivity. simpl. rewrite jump_nil;reflexivity. simpl. replace (pow_pos Zmult 0 p2) with 0. ring. clear;induction p2;simpl;auto with zarith. rewrite <- IHp2;reflexivity. Qed. Lemma strict_pos_expr_if_all_pos_aux :   forall (p:Pol Z), all_coef_pos p = true -> forall l, all_mem_pos l ->     0 < Pphi 0 Zplus Zmult (IDphi (R:=Z)) (@nil _) p ->     0< Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p. Proof.   intro p;     rewrite Pphi_nil.   induction p;simpl.   tauto.   intros H l H0 H1.   apply IHp.   assumption.   rewrite <- all_mem_pos_def in H0|-*.   intros c H2.   apply H0.   apply jump_in with (1:=H2).   destruct p0;simpl in H1.   unfold IDphi;assumption.   rewrite jump_nil in H1;assumption.   replace (pow_pos Zmult 0 p0) with 0 in H1.   rewrite Zmult_comm in H1; simpl in H1;assumption.   clear;induction p0;simpl;auto.   rewrite <- IHp0;auto.   intros H l H0 H1.   assert (0<=hd 0 l).   clear - H0.   induction l.   simpl;omega.   simpl.   rewrite <- all_mem_pos_def in H0;simpl in H0;eauto.   assert (0<=pow_pos Zmult (hd 0 l) p2).   set (u:=hd 0 l) in *;clearbody u.   clear - H2.   induction p2; simpl; auto with zarith.   assert (0<= Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p1).   eapply pos_expr_if_all_pos_aux.   symmetry in H.   destruct (@andb_true_eq _ _ H);auto.   assumption.   assert (0 < Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l) p3).   apply IHp2.   symmetry in H.   destruct (@andb_true_eq _ _ H);auto.   rewrite <- all_mem_pos_def in H0|-*.   intros c H5.   apply H0. destruct l;simpl in H5|-*. tauto. auto.   clear - H1; destruct p3;simpl in H1.   exact H1.   rewrite jump_nil in H1;assumption.   replace (pow_pos Zmult 0 p) with 0 in H1.   rewrite Zmult_comm in H1; simpl in H1;assumption.   clear;induction p;simpl;auto.   rewrite <- IHp;auto.   set (u:=pow_pos Zmult (hd 0 l) p2) in *;clearbody u.   set (v:=Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p1) in *;clearbody v.   set (w:=Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l) p3) in *;clearbody w.   clear - H3 H4 H5.   assert (0<= v*u) by auto with zarith.   auto with zarith. Qed. Lemma strict_pos_expr_if_all_pos_aux' :   forall (p:Pol Z), all_coef_pos p = true -> forall l, all_mem_pos l ->     0< @Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) nil p ->     0< @Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l p. Proof.   intros p H l H0.  replace ( @Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l p)     with (Pphi 0 Zplus Zmult (@IDphi Z) l p).  replace (Pphi_pow 0 1 Zplus Zmult Zminus Zopp 0 1 Zeq_bool      (IDphi (R:=Z)) Z_of_N Zpower (get_sign_None (C:=Z)) nil p)     with (Pphi 0 Zplus Zmult (@IDphi Z) nil p).  intro.  apply strict_pos_expr_if_all_pos_aux;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 Zopp _ InitialRing.Zsth Zeq_bool InitialRing.Zeqb_ok).   exact Zpower_theory.   constructor.   destruct c;simpl;try (intros;discriminate).  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 Zopp _ InitialRing.Zsth Zeq_bool InitialRing.Zeqb_ok).   exact Zpower_theory.   constructor.   destruct c;simpl;try (intros;discriminate). Qed. Lemma strict_pos_expr_if_all_pos' :   forall pe, all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil pe) = true ->     forall l, all_mem_pos l ->       0 < PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower (@nil Z) pe ->       0< ( PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe) . Proof.   intros p H l H0.   rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z))     (lmp:=@nil (Mon * Pol Z)) (pe:=p) (npe:=norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil       p).   rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z))     (lmp:=@nil (Mon * Pol Z)) (pe:=p) (npe:=norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil       p).   apply strict_pos_expr_if_all_pos_aux';assumption.   vm_compute;exact I.   vm_compute;reflexivity.   reflexivity.   vm_compute;exact I.   vm_compute;reflexivity.   reflexivity. Qed. Lemma strict_pos_expr_if_all_pos : forall pe1 pe2,   all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil (PEsub pe2 pe1)) = true ->   forall l, all_mem_pos l ->       PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower (@nil Z) pe1 < PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower (@nil Z) pe2 ->       PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe1 < ( PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe2) . Proof.   intros pe1 pe2 H l H0 H1.   assert (0< PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe2 -    PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe1).   replace (PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe2 -    PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe1) with   (PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l (PEsub pe2 pe1)) by (vm_compute;reflexivity).   apply strict_pos_expr_if_all_pos'.   assumption.   assumption.   simpl. auto with zarith.   auto with zarith. Qed. Ltac ring_ineq :=   match goal with     | |- ?p <= ?q =>       let mkFV := FV Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in         let mkPol := mkPolexpr Z Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in           let fv := mkFV p (@List.nil Z) in           let fv := mkFV q fv in             let pe := mkPol p fv in             let qe := mkPol q fv in               let p' := constr:(PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv pe) in                 let q' := constr:(PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv qe) in                   let H:= fresh "H" in                   (assert (H':p' <= q');[                     apply pos_expr_if_all_pos;                       [vm_compute;reflexivity| simpl;repeat split;assumption]                     | vm_compute in H';exact H'                   ])     | |- ?p < ?q =>       let mkFV := FV Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in         let mkPol := mkPolexpr Z Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in           let fv := mkFV p (@List.nil Z) in           let fv := mkFV q fv in             let pe := mkPol p fv in             let qe := mkPol q fv in               let p' := constr:(PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv pe) in                 let q' := constr:(PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv qe) in                   let H:= fresh "H" in                   (assert (H':p' < q');[                     apply strict_pos_expr_if_all_pos;                       [vm_compute;reflexivity| simpl;repeat split;assumption| vm_compute;reflexivity]                     | vm_compute in H';exact H'                   ])   end. Function all_le (l1 l2:list Z) {struct l1}: Prop :=   match l1 with     | nil =>       match l2 with         | nil => True         | _ => False       end     | x::l1 =>       match l2 with         | nil => False         | y::l2 =>           x <= y /\ all_le l1 l2       end   end . Lemma all_le_def : forall l1 l2, all_le l1 l2 <-> (length l1 = length l2 /\ forall x y, In (x,y) (combine l1 l2) -> x <= y). Proof. intros l1 l2;functional induction (all_le l1 l2). simpl;tauto. simpl. destruct l2. split;try tauto. split;try tauto. simpl;inversion 1;discriminate. simpl. split;try tauto. simpl;inversion 1;discriminate. simpl. destruct IHP as [lhs rhs]. split. intros [H1 H2]. destruct (lhs H2) as [Heq Hforall];split. f_equal. exact Heq. intros x' y' [h|h]. injection h;clear h;intros;subst;exact H1. auto. clear lhs. intros [H1 H2]. split;auto. Qed. Lemma jump_length : forall A n (l1 l2:list A), length l1 = length l2 -> length (jump n l1) = length (jump n l2). Proof.   induction n;simpl;intros l1 l2 Hlenght.   do 2 apply IHn.   destruct l1;destruct l2;simpl in Hlenght;try discriminate.   reflexivity.   simpl. injection Hlenght;auto.   do 2 apply IHn.   assumption.   destruct l1;destruct l2;simpl in Hlenght;try discriminate.   reflexivity.   simpl. injection Hlenght;auto. Qed. Lemma jump_combine :   forall A n (l1 l2:list A), jump n (combine l1 l2) = combine (jump n l1) (jump n l2). Proof.   induction n; simpl.   intros l1 l2.   do 2 rewrite <- IHn.   do 2 f_equal.   destruct l1;destruct l2;simpl;try reflexivity.   destruct l1;simpl; reflexivity.   intros l1 l2.   do 2 rewrite <- IHn.   do 2 f_equal.   intros l1 l2.   destruct l1;destruct l2;simpl;try reflexivity.   destruct l1;simpl; reflexivity. Qed. 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.   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 Zle_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 Zle_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 Zle_trans with (pow_pos Zmult z _x);auto with zarith.   apply Zle_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 Zle_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 Zle_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 Zle_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 Zle_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. 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 Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l1 p <=      @Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l2 p. Proof.   intros p H l1 l2 H0 H1.  replace (@Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l1 p)     with (Pphi 0 Zplus Zmult (@IDphi Z) l1 p).  replace (Pphi_pow 0 1 Zplus Zmult Zminus Zopp 0 1 Zeq_bool      (IDphi (R:=Z)) Z_of_N Zpower (get_sign_None (C:=Z)) 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 Zopp _ InitialRing.Zsth Zeq_bool InitialRing.Zeqb_ok).   exact Zpower_theory.   constructor.   destruct c;simpl;try (intros;discriminate).  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 Zopp _ InitialRing.Zsth Zeq_bool InitialRing.Zeqb_ok).   exact Zpower_theory.   constructor.   destruct c;simpl;try (intros;discriminate). Qed. Lemma pos_expr_incr_aux :   forall pe,   all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil pe) = true ->   forall l1 l2, all_le l1 l2 -> all_mem_pos l1 ->     0 <= PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l1 pe     <= ( PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l2 pe) . 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 (Mon * Pol Z)) (pe:=pe) (npe:=norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil       pe).   rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z))     (lmp:=@nil (Mon * Pol Z)) (pe:=pe) (npe:=norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool 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. Lemma pos_expr_incr :   forall pe,   all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil pe) = true ->   forall l1 l2, all_le l1 l2 -> all_mem_pos l1 ->     PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l1 pe     <= ( PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l2 pe) . Proof.   intros pe H l1 l2 H0 H1.   destruct (pos_expr_incr_aux pe H l1 l2 H0 H1) as [_ h];exact h. Qed. Ltac modify_FV H l :=   match l with     | nil => constr:(@nil Z)     | ?x::?l =>         match type of H with           | ?p <= x =>             match p with               | 0 => fail 1               | _ =>                 constr:(p::l)             end       end     | ?y::?l =>       let fv' := modify_FV H l in         constr:(y::fv')   end. Ltac set_as_var_if_needed p :=   let set_as_var :=     let x := fresh "x" in       assert (0<=p) by ring_ineq         in                  match p with           | context [Zplus _ _] => set_as_var           | context [Zmult _ _] => set_as_var           | context [Zminus _ _] => set_as_var           | context [Zopp _] => set_as_var           | _ => idtac         end . Ltac ring_ineq_same_pol H :=   try exact H;   match type of H with     | ?p <= ?q =>       (set_as_var_if_needed p;       set_as_var_if_needed q)   end;   match goal with     | |- ?p <= ?q =>       let mkFV := FV Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in         let mkPol := mkPolexpr Z Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in           let fv2 := mkFV q (@List.nil Z) in             let fv1 := modify_FV H fv2 in             let qe := mkPol q fv2 in               let p' := constr:(Ring_polynom.PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv1 qe) in                 let q' := constr:(Ring_polynom.PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv2 qe) in                   let H':= fresh "H" in                   (assert (H':p' <= q');[                     apply pos_expr_incr;                       [vm_compute;reflexivity|                         cbv beta iota zeta delta [all_le all_mem_pos];                           repeat split;auto with zarith|                             cbv beta iota zeta delta [all_le all_mem_pos];                           repeat split;auto with zarith                       ]                     | vm_compute in H'|-*;exact H'                   ])   end   . Ltac prove_ineq :=   match goal with     | H:?p <= ?x |- context C [ ?x ] =>       match p with         | 0 => fail 1         | _ =>           let e := context C [ x ] in             match e with               | _ <= ?e =>                 let e' := eval pattern x in e in                   match e' with                     ?f _ =>                     apply Zle_trans with (f p);                       [clear H;prove_ineq|                         let H' := fresh "H" in                           assert (H':forall a b, 0 <= a -> a <= b -> f a <= f b);                             [                               let h := fresh "h" in                                 (cbv beta;do 3 intro;intro h;ring_ineq_same_pol h)                               |                                 cbv beta in H'; refine (H' _ _ _ H);ring_ineq                             ]                       ]                   end               | _ < ?e =>                 let e' := eval pattern x in e in                   match e' with                     ?f _ =>                     apply Zlt_le_trans with (f p);                       [clear H;prove_ineq|                         let H' := fresh "H" in                           assert (H':forall a b, 0 <= a -> a <= b -> f a <= f b);                             [                               let h := fresh "h" in                                 (cbv beta;do 3 intro;intro h;ring_ineq_same_pol h)                               |                                 cbv beta in H'; refine (H' _ _ _ H);ring_ineq                             ]                       ]                   end             end       end     | _ => ring_ineq   end. Ltac soft_prove_ineq :=   match goal with     | H:?p <= ?x |- context C [ ?x ] =>       match p with         | 0 => fail 1         | _ =>           let e := context C [ x ] in             match e with               | _ <= ?e =>                 let e' := eval pattern x in e in                   match e' with                     ?f _ =>                     apply Zle_trans with (f p);                       [clear H;soft_prove_ineq| try ring_ineq_same_pol H]                   end               | _ < ?e =>                 let e' := eval pattern x in e in                   match e' with                     ?f _ =>                     apply Zlt_le_trans with (f p);                       [clear H;soft_prove_ineq| try ring_ineq_same_pol H ]                   end             end       end     | _ => try ring_ineq   end. Ltac check_pos p :=   match p with     | xH => constr:true     | xI ?p => check_pos p     | xO ?p => check_pos p     | _ => constr:false   end. Ltac check_Z n :=   match n with     | Z0 => constr:false     | Zpos ?p => check_pos p     | Zneg ?p => check_pos p     | _ => constr:false   end. Ltac simplify_one_ineq H :=   match type of H with     ?p <= ?x =>     match p with         | 0 => fail 1 | 1 => fail 1       | ?n =>         match check_Z n with           | true =>             match type of H with               ?p <= ?x =>               let e := eval pattern p in x in                 match e with                   ?f _ =>                   let f' := let f'' := eval cbv beta in (f 1) in constr:f'' in                     let prov := fresh "prov" in                       let H' := fresh "H" in                     (assert (prov:x = p*f') by ring;                       assert (H':1<= f') by omega; clear prov H;repeat rewrite Zmult_1_l in H' )||fail 1                 end             end           | false => fail 0         end     end   end . Ltac simplify_ineq := repeat (match goal with H: _ <= _ |- _ => simplify_one_ineq H end). ```