Adapt to rocq-prover/stdlib#207

Author: proux01

Coccinelle/examples/cime_trace/ring_extention.v

@@ -153,7 +153,7 @@ Qed.
 Lemma pos_expr_if_all_pos' : 
   forall pe, 
     all_coef_pos 
-    (norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.eqb Z.div_eucl ring_subst_niter nil pe) = true -> 
+    (norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.div_eucl Z.eqb ring_subst_niter nil pe) = true -> 
     forall l, all_mem_pos l  -> 
     0<= (PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower l pe) .
 Proof.
@@ -164,7 +164,7 @@ Proof.
     (lmp:=@nil (Z*Mon * Pol Z)) 
     (pe:=p) 
     (npe:=
-      norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.eqb Z.div_eucl ring_subst_niter nil
+      norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.div_eucl Z.eqb ring_subst_niter nil
         p).
   apply pos_expr_if_all_pos_aux';assumption.
   vm_compute;exact I.
@@ -176,7 +176,7 @@ Qed.
 Lemma pos_expr_if_all_pos : 
   forall pe1 pe2, 
     all_coef_pos (
-      norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.eqb Z.div_eucl ring_subst_niter
+      norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.div_eucl Z.eqb ring_subst_niter
         nil (PEsub pe2  pe1)
     ) = true -> 
     forall l, all_mem_pos l  -> 
@@ -521,7 +521,7 @@ Proof.
 Qed.
 
 Lemma strict_pos_expr_if_all_pos' : 
-  forall pe, all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.eqb Z.div_eucl ring_subst_niter nil pe) = true -> 
+  forall pe, all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.div_eucl Z.eqb ring_subst_niter nil pe) = true -> 
     forall lb, all_mem_pos lb  -> 
       forall lz, length lb = length lz -> all_mem_bounded (combine lb lz) ->
       0 < PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z)) Z_of_N Zpower lb pe -> 
@@ -531,10 +531,10 @@ Proof.
 
 
   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 Z.eqb Z.div_eucl ring_subst_niter nil
+    (lmp:=@nil (Z*Mon * Pol Z)) (pe:=pe) (npe:=norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.div_eucl Z.eqb 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 Z.eqb Z.div_eucl ring_subst_niter nil
+    (lmp:=@nil (Z*Mon * Pol Z)) (pe:=pe) (npe:=norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.div_eucl Z.eqb ring_subst_niter nil
       pe).
   apply strict_pos_expr_if_all_pos_aux';assumption.
   vm_compute;exact I.
@@ -546,7 +546,7 @@ Proof.
 Qed.
 
 Lemma strict_pos_expr_if_all_pos :   forall pe1 pe2, 
-  all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.eqb Z.div_eucl ring_subst_niter nil  (PEsub pe2 pe1)) = true -> 
+  all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.div_eucl Z.eqb ring_subst_niter nil  (PEsub pe2 pe1)) = true -> 
   forall lb, all_mem_pos lb -> 
     forall lz, length lb = length lz -> all_mem_bounded (combine lb lz) ->
       PEeval 0 1 Zplus Zmult Zminus Z.opp (IDphi (R:=Z))  Z_of_N Zpower lb pe1 < 
@@ -753,18 +753,18 @@ Qed.
 
 Lemma pos_expr_incr_aux :   
   forall pe, 
-  all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.eqb Z.div_eucl ring_subst_niter nil  pe) = true -> 
+  all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.div_eucl Z.eqb 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.
   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 Z.eqb Z.div_eucl ring_subst_niter nil
+    (lmp:=@nil (Z * Mon * Pol Z)) (pe:=pe) (npe:=norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.div_eucl Z.eqb 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 Z.eqb Z.div_eucl ring_subst_niter nil
+    (lmp:=@nil (Z* Mon * Pol Z)) (pe:=pe) (npe:=norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.div_eucl Z.eqb ring_subst_niter nil
       pe).
   apply pos_pol_incr';assumption.
   vm_compute;exact I.
@@ -777,7 +777,7 @@ Qed.
 
 Lemma pos_expr_incr :   
   forall pe, 
-  all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.eqb Z.div_eucl ring_subst_niter nil  pe) = true -> 
+  all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Z.opp Z.div_eucl Z.eqb ring_subst_niter nil  pe) = true -> 
   forall l1 l2, all_le l1 l2 -> all_mem_pos l1 -> 
     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) .