diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml
index 459c90a..02792bb 100644
--- a/.github/workflows/coq.yml
+++ b/.github/workflows/coq.yml
@@ -13,7 +13,7 @@ jobs:
       fail-fast: false
       matrix:
         include:
-          - env: { COQ_VERSION: "9.0", DOCKER_MATHCOMP_VERSION: "2.4.0" }
+          - env: { COQ_VERSION: "9.1", DOCKER_MATHCOMP_VERSION: "2.6.0" }
 
     runs-on: ubuntu-latest
     env: ${{ matrix.env }}
@@ -30,6 +30,6 @@ jobs:
 
       - uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-laproof.opam'
+          opam_file: 'rocq-laproof.opam'
           custom_image: mathcomp/mathcomp:${{ matrix.env.DOCKER_MATHCOMP_VERSION }}-rocq-prover-${{ matrix.env.COQ_VERSION }}
           export: CI
diff --git a/C/densemat_lemmas.v b/C/densemat_lemmas.v
index 84b6cda..b650242 100644
--- a/C/densemat_lemmas.v
+++ b/C/densemat_lemmas.v
@@ -139,11 +139,10 @@ lia.
   rewrite ptrofs_add_repr.
   rewrite Ptrofs.unsigned_repr by rep_lia.
   unfold natural_alignment in H2.
-  repeat apply Z.divide_add_r.
-  destruct H2 as [x ?]. rewrite H2. 
-  exists (2*x)%Z. lia.
-  exists 2; lia.
-  apply Z.divide_mul_l. exists 2; lia.
+  unfold Archi.align_float64.
+  repeat apply Z.divide_add_r; auto.
+  apply Z.divide_refl.
+  apply Z.divide_factor_l.
 - split; simpl; auto. lia.
 Qed.
 
diff --git a/C/matrix_model.v b/C/matrix_model.v
index 365114c..22e43ca 100644
--- a/C/matrix_model.v
+++ b/C/matrix_model.v
@@ -56,8 +56,8 @@ intros.
   set (H0 := ltnW _). clearbody H0.
   change (fun _ => _) with (@widen_ord k n H0).
   apply (@map_inj _ _ (@nat_of_ord n)). apply ord_inj.
-  rewrite map_take val_ord_enum take_iota /minn H /ord_enum -map_comp pmap_filter.
-  2: move => x; unfold insub; destruct idP; auto.
+  rewrite map_take val_ord_enum take_iota /minn H /ord_enum -map_comp pmap_filter;
+  try solve [move => x; unfold insub; destruct idP; auto].
   clear.
   destruct k; auto.
   set (n := S k) in *.
@@ -343,8 +343,7 @@ assert (Datatypes.is_true (leq (S (S (nat_of_ord k))) n)).
 assert (k1 = @Ordinal n (S k) H). apply ord_inj; auto.
 subst k1.
 unfold subtract_loop_jik at 1.
-rewrite (take_snoc i).
-  2: (rewrite  size_ord_enum; pose proof ltn_ord k;  lia).
+rewrite (take_snoc i); try solve [ rewrite  size_ord_enum; pose proof ltn_ord k;  lia].
 rewrite /subtract_loop !map_cat /= foldl_cat /= nth_ord_enum' //.
 Qed.
 
@@ -374,7 +373,7 @@ split; [ | split3]; intros; try split; hnf; intros; try lia.
    unfold update_mx at 1. rewrite mxE.
    destruct (Nat.eq_dec _ _); [lia  |]. simpl.
    destruct H2.
-   rewrite H1; [ |apply Hij]. f_equal.
+   rewrite H1; try solve [apply Hij]. f_equal.
    * unfold subtract_loop_jik. f_equal.
      apply eq_in_subrange.
      intros. unfold update_mx. rewrite !mxE.
diff --git a/C/verif_build_csr.v b/C/verif_build_csr.v
index 65bc55a..657bd11 100644
--- a/C/verif_build_csr.v
+++ b/C/verif_build_csr.v
@@ -61,6 +61,40 @@ replace (Zlength (coo_entries (add_to_coo coo i j x))) with (n+1)
 cancel.
 Qed.
 
+(* See:  https://github.com/PrincetonUniversity/VST/issues/869 *)
+
+Ltac freeze_tac_entail L name ::=
+  eapply (freeze_SEP''entail (map Z.to_nat L)); 
+   [solve_is_increasing
+   | match goal with |- _ = (my_freezelist_nth ?A _) => let j := eval compute in A in change A with j end;
+     cbv [my_freezelist_nth my_nth]; unfold map at 1;
+     match goal with |- _ = (_, my_delete_list ?A _) => let j := eval compute in A in change A with j end;
+     cbv [my_delete_list my_delete_nth];
+     reflexivity
+   | match goal with
+           | |- ENTAIL _, (PROPx _ (LOCALx _ (SEPx ((FRZL ?xs) :: my_delete_list ?A _)))) |-- _ =>
+           let D := fresh name in
+           set (D:=xs);
+           change xs with (@abbreviate (list mpred) xs) in D
+         end].
+
+
+Ltac freeze_tac L name ::=
+  eapply (freeze_SEP'' (map Z.to_nat L)); 
+   [solve_is_increasing
+   | match goal with |- _ = (my_freezelist_nth ?A _) => let j := eval compute in A in change A with j end;
+     cbv [my_freezelist_nth my_nth]; unfold map at 1;
+     match goal with |- _ = (_, my_delete_list ?A _) => let j := eval compute in A in change A with j end;
+     cbv [my_delete_list my_delete_nth];
+     reflexivity
+ | match goal with
+           | |- semax _ (PROPx _ (LOCALx _ (SEPx ((FRZL ?xs) ::  _)))) _ _ =>
+           let D := fresh name in
+           set (D:=xs);
+           change xs with (@abbreviate (list mpred) xs) in D
+    end
+].
+
 Lemma body_coo_count: semax_body Vprog Gprog f_coo_count coo_count_spec.
 Proof.
 start_function.
diff --git a/C/verif_densemat.v b/C/verif_densemat.v
index dc70048..3209048 100644
--- a/C/verif_densemat.v
+++ b/C/verif_densemat.v
@@ -118,10 +118,10 @@ destruct H4.
 rewrite H4.
 repeat apply Z.divide_add_r.
 apply Z.divide_mul_r.
-exists 2; auto.
-exists 2; auto.
+apply Z.divide_refl.
+apply Z.divide_refl.
 apply Z.divide_mul_l.
-exists 2; auto.
+apply Z.divide_refl.
 -
 sep_apply data_at__data_at.
 apply derives_refl'.
diff --git a/_CoqProject b/_CoqProject
index a404827..731eacc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -19,7 +19,6 @@ accuracy_proofs/gemv_acc.v
 accuracy_proofs/vec_op_acc.v
 accuracy_proofs/gemm_acc.v
 accuracy_proofs/export.v
-accuracy_proofs/libvalidsdp.v
 accuracy_proofs/solve_model.v
 
 C/floatlib.v
diff --git a/accuracy_proofs/common.v b/accuracy_proofs/common.v
index 1ff4a36..f13aad8 100644
--- a/accuracy_proofs/common.v
+++ b/accuracy_proofs/common.v
@@ -217,10 +217,10 @@ Definition default_abs : R :=
 
 Lemma default_rel_sep_0 : default_rel <> R0.
 Proof.
-  apply Rabs_lt_pos.
+  apply Rabs_lt_pos. unfold default_rel; simpl.
   rewrite Rabs_pos_eq;
-    [ apply Rmult_lt_0_compat; try Lra.nra
-    | apply Rmult_le_pos; try Lra.nra ];
+    first [apply Rmult_lt_0_compat | apply Rmult_le_pos]; (* Do it this way for backward compatibility *)
+    try Lra.nra;
     auto with commonDB.
 Qed.
 Hint Resolve default_rel_sep_0 : commonDB.
@@ -390,15 +390,17 @@ Proof.
   rewrite <- !Rmult_assoc.
   replace (bpow Zaux.radix2 1 * / 2) with 1 by (simpl; nra).
   rewrite !bpow_opp.
-  rewrite !Rcomplements.Rle_div_r.
-  - field_simplify; try nra.
-    replace 1 with (bpow Zaux.radix2 0) by (simpl; auto).
-    apply bpow_le.
-    pose proof fprec_gt_one t; lia.
-  - apply Rlt_gt.
+  rewrite !Rcomplements.Rle_div_r;
+  first [  (* do it this way for backward compatibility *)
+   apply Rlt_gt;
     replace (/ bpow Zaux.radix2 (fprec t))
-      with (1 / bpow Zaux.radix2 (fprec t)) by nra.
-    apply Rdiv_lt_0_compat; try nra.
+      with (1 / bpow Zaux.radix2 (fprec t)) by nra;
+    apply Rdiv_lt_0_compat; nra
+  | field_simplify; try nra;
+    replace 1 with (bpow Zaux.radix2 0) by (simpl; auto);
+    apply bpow_le;
+    pose proof fprec_gt_one t; lia
+ ].
 Qed.
 
 End WithType.
diff --git a/accuracy_proofs/dot_acc.v b/accuracy_proofs/dot_acc.v
index 347438c..c5a820a 100644
--- a/accuracy_proofs/dot_acc.v
+++ b/accuracy_proofs/dot_acc.v
@@ -119,7 +119,7 @@ Proof.
     assert (Heq : dotprodR (rev u) (map FT2R v2) = FT2R (dotprodF v1 v2) - eta).
     { eapply R_dot_prod_rel_eq; eauto.
       rewrite -dotprodR_rev;
-        [ | rewrite size_map; rewrite size_rev in Hsize_u; auto].
+      try solve [rewrite size_map; rewrite size_rev in Hsize_u; auto].
       rewrite -map_rev; auto. }
     nra.
   - (* per-element bound *)
@@ -127,8 +127,8 @@ Proof.
     intros n Hn.
     assert (Hlt : (size u - S n < size v2)%nat) by lia.
     specialize (Helem_bound (size u - S n)%nat Hlt).
-    rewrite nth_rev in Helem_bound; [ | rewrite Hlen' //].
-    rewrite nth_rev; [ | lia].
+    rewrite nth_rev in Helem_bound; try solve [rewrite Hlen' //].
+    rewrite nth_rev; try lia.
     destruct Helem_bound as (delta & Hval & Hdelta).
     exists delta; split.
     + rewrite Hval; repeat f_equal.
diff --git a/accuracy_proofs/dot_acc_lemmas.v b/accuracy_proofs/dot_acc_lemmas.v
index f31e80f..9be7a80 100644
--- a/accuracy_proofs/dot_acc_lemmas.v
+++ b/accuracy_proofs/dot_acc_lemmas.v
@@ -220,7 +220,7 @@ destruct Hl.
     rewrite <- !Rplus_assoc.
     replace (D * g1 n (n - 1) + g1 n (n - 1))
       with (g1 n (n - 1) * (1 + D)) by nra.
-    rewrite one_plus_d_mul_g1; [| lia].
+    rewrite one_plus_d_mul_g1; try lia.
     rewrite Rplus_assoc.
     replace (E + D * E) with ((1 + D) * E) by nra.
     eapply Rle_trans; [apply plus_d_e_g1_le; lia |].
@@ -288,7 +288,7 @@ assert (Hl : l = [] \/ l <> []).
 destruct Hl.
 - (* case: singleton list *)
   subst; simpl.
-  rewrite (R_dot_prod_rel_single rp (FR2 a)); [| auto].
+  rewrite (R_dot_prod_rel_single rp (FR2 a)); auto.
   inversion Hfp. inversion H2; subst.
   pose proof fma_accurate' (fst a) (snd a) (Zconst t 0) Hfin as Hacc.
   destruct Hacc as (e & d & Hz & He & Hd & A).
@@ -353,7 +353,8 @@ destruct Hl.
     with (D * F + ((1 + D) * g n * s1 + D * s1) +
           g1 n (n - 1) * (1 + D) + E)
     by nra.
-  rewrite one_plus_d_mul_g one_plus_d_mul_g1.
+  rewrite one_plus_d_mul_g one_plus_d_mul_g1;
+  try solve [unfold n; destruct l; try congruence; simpl; lia].
   rewrite Rplus_assoc.
   apply Rplus_le_compat; [apply Rplus_le_compat |].
   + rewrite <- Rabs_mult; fold F.
@@ -365,7 +366,6 @@ destruct Hl.
     apply Req_le; f_equal; auto; lia.
   + replace (n.+1 - 1)%nat with n by lia.
     apply plus_e_g1_le.
-  + unfold n; destruct l; try congruence; simpl; lia.
 Qed.
 
 End ForwardErrorRel2.
@@ -516,7 +516,7 @@ subst; clear Hlen1.
     destruct Hun as (delta & Hun & Hdelta).
     simpl.
     replace 0 with (Rmult (1 + d') 0) by nra.
-    rewrite (nth_map R0); [| lia].
+    rewrite (nth_map R0); try lia.
     rewrite Hun.
     exists ((1 + d') * (1 + delta) - 1).
     split; [nra |].
@@ -681,7 +681,7 @@ subst; clear Hlen1.
     specialize (B n H1).
     destruct B as (delta & B & HB); simpl.
     replace 0 with (Rmult (1 + d) 0) by nra.
-    rewrite (nth_map R0); [| lia].
+    rewrite (nth_map R0); try lia.
     rewrite B.
     exists ((1 + d) * (1 + delta) - 1).
     split; [nra |].
@@ -710,8 +710,8 @@ subst; clear Hlen1.
         rewrite Rabs_R1.
         eapply Rle_trans; [apply Rplus_le_compat_l; apply Hd |].
         apply Rle_refl. }
-    rewrite one_plus_d_mul_g1.
-    2: { destruct l; [contradiction | simpl; lia]. }
+    rewrite one_plus_d_mul_g1;
+      try solve [destruct l; [contradiction | simpl; lia]].
     unfold g1; field_simplify.
     rewrite Rplus_assoc.
     apply Rplus_le_compat.
diff --git a/accuracy_proofs/dotprod_model.v b/accuracy_proofs/dotprod_model.v
index c705fc3..25f3cc1 100644
--- a/accuracy_proofs/dotprod_model.v
+++ b/accuracy_proofs/dotprod_model.v
@@ -357,11 +357,10 @@ Proof. reflexivity. Qed.
     
 Lemma sum_rev l : sum_fold l = sum_fold (rev l).
 Proof.
-  rewrite /sum_fold -foldl_rev foldl_foldr.
+  rewrite /sum_fold -foldl_rev foldl_foldr;
+  try solve [hnf; intros; lra].
   f_equal;
     do 2 (apply FunctionalExtensionality.functional_extensionality; intro); lra.
-  hnf; intros; lra.
-  hnf; intros; lra.
 Qed.
 
 (** [R_dot_prod_rel] characterizes [dotprodR]: for any v1 and v2,
@@ -379,9 +378,8 @@ Proof.
   apply R_dot_prod_rel_cons; apply IHl.
   subst z.
   clear.
-  rewrite !foldl_foldr; [ | compute; intros; lra..].
-  destruct a as [x y]; simpl.
-  rewrite Rplus_comm //.
+  rewrite !foldl_foldr;  try solve [compute; intros; lra].
+  destruct a;  rewrite Rplus_comm //.
 Qed.
 
 (** The value of the real dot product relation is injective in s. *)
@@ -448,8 +446,8 @@ Proof.
   move :(dotprodR_rel (rev (map FT2R v1)) (rev (map FT2R v2))).
   rewrite dotprodR_rev ?size_rev ?size_map // revK
           /sum_fold /dotprodR /dotprod
-          foldl_foldr //.
-  2,3: compute; intros; lra.
+          foldl_foldr //;
+  try solve [compute; intros; lra];
   rewrite -rev_zip ?size_map ?flip_Rplus //.
 Qed.
 
@@ -489,8 +487,8 @@ Proof.
                       (rev (map Rabs (map FT2R v2)))).
   rewrite dotprodR_rev ?size_rev ?size_map // revK
           /sum_fold /dotprodR /dotprod
-          foldl_foldr //.
-  2,3: compute; intros; lra.
+          foldl_foldr //;
+  try solve [compute; intros; lra].
   rewrite -rev_zip ?size_map ?flip_Rplus //.
 Qed.
 
@@ -603,8 +601,7 @@ Proof.
   replace (Rmult a (dotprodR u v)) with (dotprodR (map (Rmult a) u) v); auto.
   clear - H.
   unfold dotprodR, dotprod.
-  rewrite !foldl_foldr.
-  2,3,4,5: compute; intros; lra.
+  rewrite !foldl_foldr; try solve [compute; intros; lra].
   revert v H; induction u; destruct v; intros; inversion H; clear H; subst;
     simpl.
   compute; lra.
@@ -822,7 +819,7 @@ Proof.
     move :H => /eqP H.
     simpl in Hlen.
     rewrite -H Rmult_0_l.
-    rewrite (IHl _ _ H0 H3). lra. lia.
+    rewrite (IHl _ _ H0 H3); try lia; lra.
 Qed.
 
 (** Absolute-value dot product analogue of [R_dot_prod_rel_nnzR]:
@@ -845,8 +842,7 @@ Proof.
     move :H => /= /andP [H H0].
     move :H => /eqP H.
     simpl in Hlen.
-    rewrite -H Rabs_R0 Rmult_0_l (IHl _ _ H0 H3).
-    lra. lia.
+    rewrite -H Rabs_R0 Rmult_0_l (IHl _ _ H0 H3); try lia; lra.
 Qed.
 
 End NonZeroDP.
\ No newline at end of file
diff --git a/accuracy_proofs/float_acc_lems.v b/accuracy_proofs/float_acc_lems.v
index 1c54cff..5a4f88f 100644
--- a/accuracy_proofs/float_acc_lems.v
+++ b/accuracy_proofs/float_acc_lems.v
@@ -308,9 +308,10 @@ Proof.
                 BinarySingleNaN.mode_NE
                 x y z Hfinx Hfiny Hfinz) as H.
   cbv zeta in H.
-  rewrite Rlt_bool_true in H.
-  - destruct H as [_ [HFIN _]]; exact HFIN.
-  - move: Hov; by rewrite /fma_no_overflow /rounded.
+  rewrite Rlt_bool_true in H;
+  first [ (* do it this way for backward compatibility *)
+    destruct H as [_ [HFIN _]]; exact HFIN
+  |  move: Hov; by rewrite /fma_no_overflow /rounded].
 Qed.
 
 
diff --git a/accuracy_proofs/fma_dot_acc.v b/accuracy_proofs/fma_dot_acc.v
index 8d0ac17..d1f9acb 100644
--- a/accuracy_proofs/fma_dot_acc.v
+++ b/accuracy_proofs/fma_dot_acc.v
@@ -79,7 +79,7 @@ Proof.
   assert (Hlenr : size (rev v1) = size (rev v2)) by (rewrite !size_rev; auto).
   rewrite <- size_rev in Hlen.
   pose proof fma_dot_prod_rel_fold_right v1 v2 as Hrel.
-  rewrite rev_zip in Hrel. 2: revert Hlen; rewrite size_rev; auto.
+  rewrite rev_zip in Hrel; try solve [revert Hlen; rewrite size_rev; auto].
   revert Hlen; rewrite size_rev; intro Hlen.
   pose proof (fma_dotprod_mixed_error_rel
                 (rev v1) (rev v2) Hlenr
@@ -103,8 +103,8 @@ Proof.
     rewrite size_rev in Hsize.
     assert (Hlt : (size u - S n < size v2)%nat) by lia.
     specialize (Hbnd (size u - S n)%nat Hlt).
-    rewrite nth_rev in Hbnd. 2: rewrite Hlen //.
-    rewrite nth_rev.          2: rewrite Hsize Hlen //.
+    rewrite nth_rev in Hbnd; try solve [rewrite Hlen //].
+    rewrite nth_rev; try solve  [rewrite Hsize Hlen //].
     destruct Hbnd as (delta & Hnth & Hdelta).
     exists delta; split.
     + rewrite Hnth; repeat f_equal.
diff --git a/accuracy_proofs/fma_is_finite.v b/accuracy_proofs/fma_is_finite.v
index 38917c6..4ca2407 100644
--- a/accuracy_proofs/fma_is_finite.v
+++ b/accuracy_proofs/fma_is_finite.v
@@ -309,8 +309,8 @@ Proof.
         } 
         apply He.
     (* Final algebraic inequality using fun_bnd structure *)
-    rewrite sqrt_def.
-    { unfold fun_bnd.
+    rewrite sqrt_def; try solve [apply fun_bound_pos; auto].
+      unfold fun_bnd.
       replace (length (a :: l)) with (S n) by (simpl; lia).
       set (x := (@g t (S n - 1) + 1)).
       set (y := (1 + INR (S n) * x)).
@@ -375,7 +375,6 @@ Proof.
               | apply le_INR; lia
               | replace (S n - 1)%nat with n%nat by lia; nra ].
           + unfold n; apply lt_INR; lia. } }
-    apply fun_bound_pos; auto. }
 Qed.
 
 End NAN.
\ No newline at end of file
diff --git a/accuracy_proofs/gemv_acc.v b/accuracy_proofs/gemv_acc.v
index caa3bb5..b54355b 100644
--- a/accuracy_proofs/gemv_acc.v
+++ b/accuracy_proofs/gemv_acc.v
@@ -44,7 +44,7 @@ From LAProof.accuracy_proofs Require Import preamble common
                                              dotprod_model sum_model
                                              dot_acc float_acc_lems mv_mathcomp.
 
-From mathcomp.algebra_tactics Require Import ring.
+From mathcomp.algebra Require Import ring_tactic.
 
 Section WithNAN.
 
@@ -89,8 +89,7 @@ Proof.
     rewrite (unlock (bigop_unlock)).
     unfold reducebig, comp, applybig.
     unfold dotprodR, dotprod.
-    rewrite foldl_foldr.
-    2, 3: compute; intros; lra.
+    rewrite foldl_foldr; try solve [ compute; intros; lra].
     unfold seq_of_rV.
     rewrite -!map_comp.
     rewrite /seq_of_rV size_map size_ord_enum in Hu.
@@ -112,8 +111,7 @@ Proof.
     rewrite {}Hval.
     unfold seq_of_rV in Hbd |- *.
     rewrite size_map size_ord_enum in Hbd.
-    rewrite (nth_map j).
-    2: { rewrite size_ord_enum; pose proof (ltn_ord j); lia. }
+    rewrite (nth_map j); try solve [rewrite size_ord_enum; pose proof (ltn_ord j); lia].
     rewrite nth_ord_enum'.
     change (A 0 j)%Ri with (A ord0 j).
     set Aj := FT2R (A ord0 j).
@@ -220,7 +218,8 @@ Proof.
   set Ar := map_mx FT2R A.
   set Br := map_mx FT2R B.
   have H0 : (Ar *m Br + E *m Br + eta - Ar *m Br = E *m Br + eta)%Ri.
-  { rewrite -!addrA addrC addrA -addrA addNr addr0 //. }
+  rewrite -addrA (addrC eta) addrA; f_equal.
+  rewrite -!addrA addrC -addrA addNr addr0 //.
   rewrite {}H0.
   eapply (le_trans (normv_triang _ _ _)).
   apply lerD.
@@ -228,15 +227,17 @@ Proof.
   apply ler_pM => //.
   apply normM_pos.
   apply normv_pos.
-  rewrite /normM mulrC big_max_mul.
+  rewrite /normM mulrC big_max_mul; try solve [apply /RleP; auto with commonDB].
   apply: le_bigmax2 => i0 _.
   rewrite /sum_abs.
-  rewrite big_mul => [ | i b | ]; [ | ring | ].
-  - apply ler_sum => i _.
+   rewrite big_mul.
+   move => i b ; ring.
+   apply /RleP; auto with commonDB.  
+  apply ler_sum => i _.
     rewrite mulrC -/Ar //.
-  - apply /RleP; auto with commonDB.
-  - apply /RleP; auto with commonDB.
+   apply /RleP; auto with commonDB.
   - rewrite /normv.
+  apply /RleP.
      apply @bigmax_le => [ | i _].
     apply /RleP; auto with commonDB.
     auto.
diff --git a/accuracy_proofs/mv_mathcomp.v b/accuracy_proofs/mv_mathcomp.v
index 829b689..1a8f972 100644
--- a/accuracy_proofs/mv_mathcomp.v
+++ b/accuracy_proofs/mv_mathcomp.v
@@ -40,7 +40,7 @@
 From LAProof.accuracy_proofs Require Import preamble common
     dotprod_model sum_model dot_acc float_acc_lems.
 
-From mathcomp.algebra_tactics Require Import ring.
+(* From mathcomp.algebra_tactics Require Import ring. *)
 
 Open Scope ring_scope.
 Open Scope order_scope.
@@ -391,7 +391,8 @@ Proof.
     change (0 <= 0 * xx)%Re.
     rewrite Rmult_0_l; reflexivity.
   - remember (normv u) as umax.
-    rewrite /normr /normM /normv /sum_abs /= big_max_mul.
+    rewrite /normr /normM /normv /sum_abs /= big_max_mul;
+  try solve [rewrite Hequmax;   apply normv_pos].
     apply: le_bigmax2 => i0 _.
     rewrite mxE => /=.
     eapply le_trans; [apply Rabs_sum |].
@@ -405,8 +406,6 @@ Proof.
       1, 2: apply /RleP; apply Rabs_pos.
       rewrite Hequmax /normv.
       by apply /le_bigmax.
-    + rewrite Hequmax.
-      apply normv_pos.
 Qed.
 
 (** Triangle inequality for [normv]: [‖u + v‖_∞ ≤ ‖u‖_∞ + ‖v‖_∞]. *)
@@ -495,8 +494,8 @@ Proof.
     transitivity (map (fun y => subn n (S y)) (map (@nat_of_ord n) (ord_enum n))).
     2: { rewrite -map_comp /comp //. }
     unfold ord_enum.
-    rewrite pmap_filter.
-    2: { intro; simpl; unfold insub; destruct idP; simpl in *; auto. }
+    rewrite pmap_filter;
+      try solve [intro; simpl; unfold insub; destruct idP; simpl in *; auto].
     transitivity (map (fun y => subn n (S y)) (iota 0 n)).
     2: {
       set u := O.
@@ -522,12 +521,11 @@ Proof.
     - rewrite size_rev size_map //.
     - intros i Hi.
       rewrite size_rev size_iota in Hi.
-      rewrite -!nth_List_nth nth_rev.
-      2: rewrite size_iota; lia.
-      rewrite size_iota nth_iota.
-      2: lia.
-      rewrite (nth_map O).
-      2: rewrite size_iota; lia.
+      rewrite -!nth_List_nth nth_rev;
+      try solve [ rewrite size_iota; lia].
+      rewrite size_iota nth_iota; try lia.
+      rewrite (nth_map O);
+      try solve [rewrite size_iota; lia].
       rewrite nth_iota; try lia.
   }
   set a := rev (ord_enum n) in Hnat |-*; clearbody a.
@@ -814,7 +812,7 @@ Proof.
     f_equal; f_equal.
     apply FunctionalExtensionality.functional_extensionality; intro j.
     rewrite map_comp /comp val_ord_enum.
-    rewrite map_nth_iota; [| lia].
+    rewrite map_nth_iota; try lia.
     rewrite drop0.
     replace (take rows mval) with mval.
     2: rewrite Hrows take_size //.
@@ -844,10 +842,8 @@ Proof.
   intros.
   apply matrixP => i j.
   rewrite /mx_of_listlist mxE /listlist_of_mx.
-  rewrite (nth_map i).
-  2: rewrite size_ord_enum; apply ltn_ord.
-  rewrite (nth_map j).
-  2: rewrite size_ord_enum; apply ltn_ord.
+  rewrite (nth_map i); try solve [rewrite size_ord_enum; apply ltn_ord].
+  rewrite (nth_map j); try solve [rewrite size_ord_enum; apply ltn_ord].
   rewrite !nth_ord_enum'; auto.
 Qed.
 
@@ -870,7 +866,7 @@ Proof.
     rewrite (nth_ord_enum_lemma d vval) -Hsize.
     f_equal; f_equal.
     rewrite map_comp /comp val_ord_enum.
-    rewrite map_nth_iota; [| lia].
+    rewrite map_nth_iota; try lia.
     rewrite drop0 take_size.
     apply FunctionalExtensionality.functional_extensionality; intro j.
     rewrite mxE //.
@@ -885,8 +881,7 @@ Proof.
   intros.
   apply matrixP => i j.
   rewrite /mx_of_listlist mxE /listlist_of_mx.
-  rewrite (nth_map i).
-  2: rewrite size_ord_enum; apply ltn_ord.
+  rewrite (nth_map i); try solve [rewrite size_ord_enum; apply ltn_ord].
   rewrite !ord1.
   f_equal.
   apply nth_ord_enum'.
@@ -985,15 +980,13 @@ Proof.
       destruct (i < n1)%N eqn:Hlt.
       * unfold split; simpl.
         destruct (ltnP i n1); try lia.
-        rewrite (nth_map (Ordinal i0)).
-        2: rewrite size_ord_enum //.
+        rewrite (nth_map (Ordinal i0)); try solve [rewrite size_ord_enum //].
         change i with (nat_of_ord (Ordinal i0)).
         rewrite nth_ord_enum' //.
       * unfold split; simpl.
         destruct (ltnP i n1); try lia.
         assert (Hlt2 : is_true (i - n1 < n2)%N) by lia.
-        rewrite (nth_map (Ordinal Hlt2)).
-        2: rewrite size_ord_enum //.
+        rewrite (nth_map (Ordinal Hlt2)); try solve [rewrite size_ord_enum //].
         change (i - n1)%nat with (nat_of_ord (Ordinal Hlt2)).
         rewrite nth_ord_enum' //.
         f_equal; apply ord_inj; simpl; auto.
@@ -1062,8 +1055,7 @@ Proof.
           rewrite -nth_List_nth in HB; auto.
       }
       rewrite size_map size_ord_enum => j Hj.
-      rewrite (nth_map (Ordinal Hj)).
-      2: rewrite size_ord_enum //.
+      rewrite (nth_map (Ordinal Hj)); try solve [ rewrite size_ord_enum //].
       change j with (nat_of_ord (Ordinal Hj)).
       rewrite nth_ord_enum'.
       assert (Hnth : nth (Ordinal Hi) (ord_enum (n1 + n2)) i = Ordinal Hi).
@@ -1073,23 +1065,19 @@ Proof.
       destruct (i < n1)%N eqn:Hlt.
       * unfold split; simpl.
         destruct (ltnP i n1); try lia.
-        rewrite (nth_map (Ordinal i0)).
-        2: rewrite size_ord_enum //.
+        rewrite (nth_map (Ordinal i0)); try solve [rewrite size_ord_enum //].
         change i with (nat_of_ord (Ordinal i0)).
         rewrite nth_ord_enum' //.
-        rewrite (nth_map (Ordinal Hj)).
-        2: rewrite size_ord_enum //.
+        rewrite (nth_map (Ordinal Hj)); try solve [rewrite size_ord_enum //].
         change j with (nat_of_ord (Ordinal Hj)).
         rewrite nth_ord_enum' //.
       * unfold split; simpl.
         destruct (ltnP i n1); try lia.
         assert (Hlt2 : is_true (i - n1 < n2)%N) by lia.
-        rewrite (nth_map (Ordinal Hlt2)).
-        2: rewrite size_ord_enum //.
+        rewrite (nth_map (Ordinal Hlt2)); try solve [rewrite size_ord_enum //].
         change (i - n1)%nat with (nat_of_ord (Ordinal Hlt2)).
         rewrite nth_ord_enum' //.
-        rewrite (nth_map (Ordinal Hj)).
-        2: rewrite size_ord_enum //.
+        rewrite (nth_map (Ordinal Hj)); try solve [rewrite size_ord_enum //].
         f_equal; apply ord_inj; simpl; auto.
         change j with (nat_of_ord (Ordinal Hj)).
         rewrite nth_ord_enum' //.
@@ -1115,8 +1103,8 @@ Proof.
     rewrite /listlist_of_mx in Hnth.
     pose proof (ltn_ord i) as Hi.
     pose proof (ltn_ord j) as Hj.
-    rewrite !(nth_map i) in Hnth. 2, 3: rewrite size_ord_enum; auto.
-    rewrite !(nth_map j) in Hnth. 2, 3: rewrite size_ord_enum; auto.
+    rewrite !(nth_map i) in Hnth; try solve [rewrite size_ord_enum; auto].
+    rewrite !(nth_map j) in Hnth; try solve [rewrite size_ord_enum; auto].
     rewrite !nth_ord_enum' in Hnth.
     auto.
 Qed.
@@ -1211,9 +1199,9 @@ Proof.
         rewrite nth_seq_of_rV !mxE //.
     + change (S (size l)) with (addn 1 (size l)).
       apply listlist_of_mx_inj.
-      rewrite listlist_of_mx_of_listlist.
-      2: simpl; change @length with @size; lia.
-      2: constructor; auto.
+      rewrite listlist_of_mx_of_listlist;
+       try (simpl; change @length with @size; lia);
+      try solve [constructor; auto].
       rewrite listlist_of_mx_col_mx.
       rewrite !listlist_of_mx_of_listlist; auto.
       constructor; auto.
diff --git a/accuracy_proofs/solve_model.v b/accuracy_proofs/solve_model.v
index 960443b..204d53a 100644
--- a/accuracy_proofs/solve_model.v
+++ b/accuracy_proofs/solve_model.v
@@ -172,8 +172,7 @@ rewrite H.
 lia.
 rewrite -nth_List_nth.
 rewrite nth_take; auto.
-rewrite (nth_map i).
-rewrite nth_ord_enum' //.
+rewrite (nth_map i); try solve [rewrite nth_ord_enum' //].
 rewrite size_ord_enum.
 lia.
 Qed.
@@ -307,7 +306,7 @@ apply FunctionalExtensionality.functional_extensionality; intro i.
 unfold backward_subst_step.
 apply FunctionalExtensionality.functional_extensionality; intro z.
 f_equal.
-rewrite -Hij; [ | lia].
+rewrite -Hij; try lia.
 f_equal.
 f_equal.
 apply map_ext_in; intros.
@@ -324,7 +323,7 @@ assert (u < n \/ u >= n)%nat by lia.
 destruct H2.
 ordify n u.
 rewrite nth_ord_enum' in H0. subst. lia.
-rewrite nth_default in H0. subst; lia.
+rewrite nth_default in H0; try (subst; lia).
 rewrite size_ord_enum. lia.
 Qed.
 
@@ -339,7 +338,7 @@ apply FunctionalExtensionality.functional_extensionality; intro i.
 unfold forward_subst_step.
 apply FunctionalExtensionality.functional_extensionality; intro z.
 f_equal.
-rewrite -Hij; [ | lia].
+rewrite -Hij; try lia.
 f_equal.
 f_equal.
 apply map_ext_in; intros.
@@ -359,7 +358,7 @@ rewrite nth_take; auto.
 pose proof ltn_ord z.
 ordify n k.
 rewrite nth_ord_enum'. lia.
-rewrite nth_default. lia.
+rewrite nth_default; try lia.
 rewrite size_take. rewrite size_ord_enum.
 rewrite ltn_ord. subst. lia.
 Qed.
diff --git a/accuracy_proofs/sum_acc.v b/accuracy_proofs/sum_acc.v
index 7d38c1a..b256868 100644
--- a/accuracy_proofs/sum_acc.v
+++ b/accuracy_proofs/sum_acc.v
@@ -111,14 +111,14 @@ induction (rev x) as [| a l] => Hfin; clear x.
       rewrite nth_cat.
       rewrite size_cat size_map in Hn |- *; simpl size in Hn.
       destruct (n < size l')%N eqn:Hn_lt.
-      -- rewrite (nth_map R0); [| lia].
+      -- rewrite (nth_map R0); try lia.
          specialize (Hdel n Hn_lt).
          destruct Hdel as (d & Hd1 & Hd2).
          exists ((1+d') * (1+d) - 1).
          rewrite {}Hd1; split.
          ++ fold (ftype t).
             rewrite rev_cons nth_rcons size_rev.
-            destruct (n < size l)%N eqn:Hn'; [| lia]; nra.
+            destruct (n < size l)%N eqn:Hn';  try lia; nra.
          ++ field_simplify_Rabs.
             eapply Rle_trans;
               [apply Rabs_triang |
@@ -138,7 +138,7 @@ induction (rev x) as [| a l] => Hfin; clear x.
             rewrite Rmult_1_r /=; f_equal; lia.
       -- fold (ftype t).
          assert (Hn_eq : n = size l') by lia; subst n.
-         rewrite nth_rev /=; [| lia].
+         rewrite nth_rev /=;  try lia.
          rewrite -Hlen'; do 2 replace (_ - _)%N with O by lia; simpl.
          exists d'; split; auto.
          eapply Rle_trans; [apply Hd' |].
@@ -181,8 +181,8 @@ exists (nth R0 x'); split.
   clear H3; f_equal; f_equal; clear.
   destruct (size x'); clear x'.
   { simpl; destruct i; lia. }
-  rewrite (nth_map (@ord0 n) common.neg_zero).
-  rewrite mv_mathcomp.nth_ord_enum' //.
+  rewrite (nth_map (@ord0 n) common.neg_zero);
+  try solve [rewrite mv_mathcomp.nth_ord_enum' //].
   rewrite mv_mathcomp.size_ord_enum.
   pose proof ltn_ord i; lia.
 Qed.
@@ -290,13 +290,13 @@ end.
 - apply eq_bigr => i _.
   destruct n; [destruct i; lia |].
   rewrite -map_comp.
-  rewrite (nth_map (@ord0 n) R0).
-  rewrite mv_mathcomp.nth_ord_enum' //.
+  rewrite (nth_map (@ord0 n) R0);
+   try solve [rewrite mv_mathcomp.nth_ord_enum' //].
   rewrite mv_mathcomp.size_ord_enum //.
 - apply eq_bigr => i _.
   destruct n; [destruct i; lia |].
-  rewrite (nth_map (@ord0 n) R0).
-  rewrite mv_mathcomp.nth_ord_enum' //.
+  rewrite (nth_map (@ord0 n) R0);
+   try solve [rewrite mv_mathcomp.nth_ord_enum' //].
   rewrite mv_mathcomp.size_ord_enum //.
 Qed.
 
@@ -339,7 +339,7 @@ Theorem sum_forward_error_permute :
 Proof.
 move=> x x0 Hfin Hfin0 Hper.
 rewrite (sumR_permute (map FT2R x) (map FT2R x0));
-  [| apply Permutation_map; auto].
+   try solve [apply Permutation_map; auto].
 eapply Rle_trans; [apply sum_forward_error_permute'; eauto |].
 apply Req_le; f_equal; symmetry.
 f_equal; apply Permutation_length; auto.
diff --git a/accuracy_proofs/sum_is_finite.v b/accuracy_proofs/sum_is_finite.v
index ff9884d..f474515 100644
--- a/accuracy_proofs/sum_is_finite.v
+++ b/accuracy_proofs/sum_is_finite.v
@@ -295,7 +295,7 @@ Proof.
     apply Rlt_le_trans with (bpow Zaux.radix2 (femax t) / y * y).
     { apply Rmult_lt_compat_l; [| exact Hineq].
       unfold Rdiv; apply Rmult_lt_0_compat; [apply bpow_gt_0 | apply Rinv_pos; exact Hy]. }
-    unfold Rdiv; rewrite Rmult_assoc; rewrite Rinv_l; [lra | exact Hy'].
+    unfold Rdiv; rewrite Rmult_assoc; rewrite Rinv_l; try lra; exact Hy'.
 Qed.
 
 End NAN.
\ No newline at end of file
diff --git a/accuracy_proofs/sum_model.v b/accuracy_proofs/sum_model.v
index 39cd338..0e891cc 100644
--- a/accuracy_proofs/sum_model.v
+++ b/accuracy_proofs/sum_model.v
@@ -402,12 +402,10 @@ Lemma sumR_le_sumRabs :
 Proof.
   induction x; simpl; [nra |].
   rewrite sumRabs_Rabs in IHx.
+  eapply Rle_trans; [ apply Rabs_triang | ].
   eapply Rle_trans.
-  2: rewrite Rabs_pos_eq.
-  - apply Rabs_triang.
-  - apply Rplus_le_compat_l; auto.
-  - apply Rplus_le_le_0_compat;
-      [apply Rabs_pos | apply sumRabs_pos].
+  apply Rplus_le_compat_l; try eassumption.
+  apply Rle_abs.
 Qed.
 
 (** Inserting an element at an arbitrary position in a split list preserves
diff --git a/coq-laproof.opam b/rocq-laproof.opam
similarity index 76%
rename from coq-laproof.opam
rename to rocq-laproof.opam
index 5192346..d1154f1 100644
--- a/coq-laproof.opam
+++ b/rocq-laproof.opam
@@ -20,21 +20,21 @@ install: [
   [ make "-j%{jobs}%" "install" ]
 ]
 depends: [
-  "coq" {>= "9.0"}
+  "coq-core" {>= "9.1~"}
+  "rocq-stdlib"
   "coq-flocq"
   "coq-interval"
-  "coq-vcfloat" {>= "2.4.1~"}
-  "coq-mathcomp-ssreflect" {>= "2.4.0~"}
-  "coq-mathcomp-algebra"
-  "coq-mathcomp-analysis"
-  "coq-mathcomp-algebra-tactics"
-  "coq-mathcomp-reals-stdlib"
+  "coq-vcfloat" {>= "2.4.2~"}
+  "rocq-mathcomp-ssreflect" {>= "2.6.0~"}
+  "rocq-mathcomp-algebra"
+  "rocq-mathcomp-reals-stdlib"
+  "rocq-mathcomp-zify"
   "coq-mathcomp-finmap"
-  "coq-vst" {>= "2.16~"}
+  "coq-libvalidsdp"
+  "coq-vst" {>= "2.17"}
   "coq-vst-lib" {>= "2.15.1~"}
-  "coq-libvalidsdp" {>= "1.1.1"}
 ]
 tags: [
-  "date:2025-05-08"
+  "date:2026-09-25"
   "logpath:LAProof"
 ]