diff --git a/proofs/parity.dfy b/proofs/parity.dfy
new file mode 100644
index 0000000..22b2ca6
--- /dev/null
+++ b/proofs/parity.dfy
@@ -0,0 +1,8 @@
+lemma {:induction false} ParityProof(x: nat, y: nat) 
+    requires isEven(x) || isEven(y)
+    ensures isEven(x * y)
+    decreases x + y
+{
+    
+}
+
diff --git a/testcases/parity.dfy b/testcases/parity.dfy
new file mode 100644
index 0000000..51acfec
--- /dev/null
+++ b/testcases/parity.dfy
@@ -0,0 +1,14 @@
+predicate {:induction false} isEven(n: nat)
+{
+    if n == 0 then true 
+    else if n == 1 then false 
+    else isEven(n - 2)
+}
+
+method {:induction false} ParityTest(x: nat, y: nat) 
+    requires isEven(x) || isEven(y)
+{
+    assert isEven(x * y) by {
+        ParityProof(x, y);
+    }
+}