diff --git a/proofs/max_min_properties.dfy b/proofs/max_min_properties.dfy
new file mode 100644
index 0000000..3da9c10
--- /dev/null
+++ b/proofs/max_min_properties.dfy
@@ -0,0 +1,24 @@
+lemma {:induction false} MaxMin_Bounds(a: int, b: int)
+  ensures Max(a, b) >= a
+  ensures Max(a, b) >= b
+  ensures Min(a, b) <= a
+  ensures Min(a, b) <= b
+  ensures Max(a, b) == a || Max(a, b) == b
+  ensures Min(a, b) == a || Min(a, b) == b
+{
+}
+
+lemma {:induction false} MaxMin_Symmetry(a: int, b: int)
+  ensures Max(a, b) == Max(b, a)
+  ensures Min(a, b) == Min(b, a)
+  ensures Max(a, a) == a
+  ensures Min(a, a) == a
+{
+}
+
+lemma {:induction false} MaxMin_Relation(a: int, b: int)
+  ensures a <= b ==> Max(a, b) == b && Min(a, b) == a
+  ensures b <= a ==> Max(a, b) == a && Min(a, b) == b
+{
+}
+
diff --git a/testcases/max_min_properties.dfy b/testcases/max_min_properties.dfy
new file mode 100644
index 0000000..2fd5309
--- /dev/null
+++ b/testcases/max_min_properties.dfy
@@ -0,0 +1,59 @@
+function {:induction false} Max(a: int, b: int): int
+{
+  if a >= b then a else b
+}
+
+function {:induction false} Min(a: int, b: int): int
+{
+  if a <= b then a else b
+}
+
+// Test 1: bounds + “returns one of the arguments”.
+method {:induction false} Test_MaxMin_Bounds(a: int, b: int)
+{
+  assert
+    Max(a, b) >= a &&
+    Max(a, b) >= b &&
+    Min(a, b) <= a &&
+    Min(a, b) <= b &&
+    (Max(a, b) == a || Max(a, b) == b) &&
+    (Min(a, b) == a || Min(a, b) == b)
+  by
+  {
+    MaxMin_Bounds(a, b);
+  }
+}
+
+// Test 2: commutativity + idempotence.
+method {:induction false} Test_MaxMin_Symmetry(a: int, b: int)
+{
+  assert
+    Max(a, b) == Max(b, a) &&
+    Min(a, b) == Min(b, a) &&
+    Max(a, a) == a &&
+    Min(a, a) == a
+  by
+  {
+    MaxMin_Symmetry(a, b);
+  }
+}
+
+// Test 3: case-wise behavior (ordering).
+method {:induction false} Test_MaxMin_Relation(a: int, b: int)
+{
+  if a <= b {
+    assert Max(a, b) == b && Min(a, b) == a
+    by
+    {
+      MaxMin_Relation(a, b);
+    }
+  } else {
+    assert Max(a, b) == a && Min(a, b) == b
+    by
+    {
+      MaxMin_Relation(a, b);
+    }
+  }
+}
+
+