fixed warnings in algebrahelpers

nvaishampayan517 · nvaishampayan517 · commit 21b3483799f9 · 2024-03-31T13:04:40.000-07:00
diff --git a/AlgebraHelpers.v b/AlgebraHelpers.v
@@ -698,7 +698,7 @@ b <> 0 -> d <> 0 -> (a/b * (c/d) = (a*c)/(b*d))%R.
 Proof.
 intros.
 unfold Rdiv.
-rewrite Rinv_mult_distr. 2,3: assumption.
+rewrite Rinv_mult.
 lra.
 Qed.
 
