Commit baf0ed77 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Ensured compatibility with both 8.3 and 8.3.

parent 88bb5ac9
...@@ -1512,6 +1512,7 @@ case Zle_bool_spec ; intros Hs. ...@@ -1512,6 +1512,7 @@ case Zle_bool_spec ; intros Hs.
apply Zle_antisym. apply Zle_antisym.
cut (x / (2^mw * 2^ew) < 2)%Z. clear ; omega. cut (x / (2^mw * 2^ew) < 2)%Z. clear ; omega.
apply Zdiv_lt_upper_bound. apply Zdiv_lt_upper_bound.
try apply Hx. (* 8.2/8.3 compatibility *)
now apply Zmult_lt_0_compat. now apply Zmult_lt_0_compat.
rewrite <- Zpower_exp ; try ( apply Zle_ge ; apply Zlt_le_weak ; assumption ). rewrite <- Zpower_exp ; try ( apply Zle_ge ; apply Zlt_le_weak ; assumption ).
change 2%Z at 1 with (Zpower 2 1). change 2%Z at 1 with (Zpower 2 1).
...@@ -1521,6 +1522,7 @@ discriminate. ...@@ -1521,6 +1522,7 @@ discriminate.
apply Zle_ge. apply Zle_ge.
now apply Zplus_le_0_compat ; apply Zlt_le_weak. now apply Zplus_le_0_compat ; apply Zlt_le_weak.
apply Zdiv_le_lower_bound. apply Zdiv_le_lower_bound.
try apply Hx. (* 8.2/8.3 compatibility *)
now apply Zmult_lt_0_compat. now apply Zmult_lt_0_compat.
now rewrite Zmult_1_l. now rewrite Zmult_1_l.
apply Zdiv_small. apply Zdiv_small.
......
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