diff options
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/RIneq.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index b444d443d..acc9fd5d6 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -812,7 +812,7 @@ Hint Resolve Rinv_involutive: real. Lemma Rinv_mult_distr : forall r1 r2, r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2. Proof. - intros; field; auto. + intros; field; auto. Qed. (*********) |