Commit 7afc5cc5 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Weaken hypothesis of le_pred_lt.

parent b6bc4d4e
......@@ -918,7 +918,7 @@ apply Ropp_lt_contravar.
now apply Heps.
Qed.
Theorem le_pred_lt:
Theorem le_pred_lt_aux :
forall x y,
F x -> F y ->
(0 < x < y)%R ->
......@@ -1033,4 +1033,19 @@ now apply Rlt_Rminus.
now apply Rlt_le.
Qed.
Theorem le_pred_lt :
forall x y,
F x -> F y ->
(0 < y)%R ->
(x < y)%R ->
(x <= pred y)%R.
Proof.
intros x y Fx Fy Hy Hxy.
destruct (Rle_or_lt x 0) as [Hx|Hx].
apply Rle_trans with (1 := Hx).
now apply pred_ge_0.
apply le_pred_lt_aux ; try easy.
now split.
Qed.
End Fcore_ulp.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment