Commit a86c150e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Simplified proof.

parent 401b2cc8
......@@ -929,7 +929,7 @@ intros x.
rewrite <- (Ropp_involutive x).
rewrite round_UP_opp.
apply Rnd_DN_UP_pt_sym.
apply generic_format_satisfies_any.
apply generic_format_opp.
apply generic_DN_pt.
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