cleanup

IBM · Apr 27, 2024 · 011a25f · 011a25f
1 parent 26d2aa3
commit 011a25f
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/coq/FHE/arith.v b/coq/FHE/arith.v
@@ -2576,10 +2576,8 @@ Proof.
     rewrite /Rminus Rplus_add !Ropp_opp.
     eapply Order.POrderTheory.le_trans; cycle 1.
     apply H.
-    rewrite Order.POrderTheory.le_eqVlt.
-    apply /orP.
-    left.
-    apply /eqP.
+    apply /RlebP.
+    right.
     f_equal.
     ring.
   - apply nearest_round_leq.