more lemmas on Real.abs

00258be3 · MARCHE Claude · 7a62e628 · 00258be3
Commit 00258be3 authored Nov 28, 2011 by MARCHE Claude
Hide whitespace changes
Inline Side-by-side

Showing with 7 additions and 0 deletions

theories/real.why theories/real.why +7 -0

No files found.
--- a/theories/real.why
+++ b/theories/real.why
@@ -48,6 +48,13 @@ theory Abs
  lemma Abs_zero: forall x:real. abs x = 0.0 -> x = 0.0
 *)

+  lemma Abs_sum: forall x y:real. abs(x+y) <= abs x + abs y
+
+  lemma Abs_prod: forall x y:real. abs(x*y) = abs x * abs y
+
+  lemma triangular_inequality:
+    forall x y z:real. abs(x-z) <= abs(x-y) + abs(y-z)
+
 end

 theory MinMax