Complete 138

tasks/human_eval_138.rs

@@ -9,7 +9,13 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn is_equal_to_sum_even(n: u32) -> (b: bool)
+    ensures
+        b <==> n % 2 == 0 && n >= 8  // 2 + 2 + 2 + (n - 6)
+        ,
+{
+    n % 2 == 0 && n >= 8
+}
 
 } // verus!
 fn main() {}