Added rounding extensionality.

7b301bb5 · Guillaume Melquiond · c74e88d4 · 7b301bb5
Commit 7b301bb5 authored Aug 26, 2010 by Guillaume Melquiond
Show whitespace changes
Inline Side-by-side

Showing with 11 additions and 0 deletions

src/Core/Fcore_generic_fmt.v src/Core/Fcore_generic_fmt.v +11 -0

No files found.
--- a/src/Core/Fcore_generic_fmt.v
+++ b/src/Core/Fcore_generic_fmt.v
@@ -552,6 +552,17 @@ Qed.

 End Fcore_generic_rounding_pos.

+Theorem rounding_ext :
+  forall rnd1 rnd2,
+  ( forall x e, Zrnd rnd1 x e = Zrnd rnd2 x e ) ->
+  forall x,
+  rounding rnd1 x = rounding rnd2 x.
+Proof.
+intros rnd1 rnd2 Hext x.
+unfold rounding.
+now rewrite Hext.
+Qed.
+
 Section Zrounding_opp.

 Variable rnd : Zrounding.