diff options
Diffstat (limited to 'theories/Reals/RIneq.v')
| -rw-r--r-- | theories/Reals/RIneq.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index de41fd3f61..70f4ff0d9b 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1717,7 +1717,8 @@ Qed. Lemma plus_IZR_NEG_POS : forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q). Proof. - intros p q; simpl. case Pcompare_spec; intros H; simpl. + intros p q; simpl. rewrite Z.pos_sub_spec. + case Pcompare_spec; intros H; simpl. subst. ring. rewrite Pminus_minus by trivial. rewrite minus_INR by (now apply lt_le_weak, Plt_lt). |