Commit bcbcde24 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Adapt to Coq 8.5.

parent 38d09de5
......@@ -1135,8 +1135,7 @@ 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.
apply le_pred_lt_aux ; try easy ; now split.
Qed.
......
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