Commit de116efc authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Make a realization compatible with older versions of Coq

parent 95afb215
......@@ -123,6 +123,6 @@ rewrite <- with (1 := h2).
rewrite <- pow_IZR.
rewrite <- INR_IZR_INZ.
apply Rpower_pow.
now apply IZR_lt.
now apply (IZR_lt 0).
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