diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index bab9e05ecf91a2b75e6a4f466a574eb987007bf0..d581fcd571e79324326d1e822d433255bedebb13 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -346,21 +346,22 @@ let phi_addr_of_int p =
 (* -------------------------------------------------------------------------- *)
 
 (* Lemmas proved with Memory definition:
-   - lemma valid_rd_null: forall m n. n <= 0 -> valid_rd m null n
-   - lemma valid_rw_null: forall m n. n <= 0 -> valid_rw m null n *)
+   - lemma valid_rd_null: forall m n. n <= 0 <-> valid_rd m null n
+   - lemma valid_rw_null: forall m n. n <= 0 <-> valid_rw m null n *)
 let r_valid_unref = function
   | [_; p; n] when p == a_null -> e_leq n e_zero
   | _ -> raise Not_found
 
-(* Lemmas proved with Memory definition:
+(* Lemma proved with Memory definition:
    - lemma valid_obj_null: forall m n. valid_obj m null n *)
 let r_valid_obj = function
   | [_; p; _] when p == a_null -> e_true
   | _ -> raise Not_found
 
-(* Condition: by definition of 'invalid_null' *)
+(* Lemma proved with Memory definition:
+   - lemma invalid_null: forall m n. 0 < n <-> invalid m null n *)
 let r_invalid = function
-  | [_; p; n] when p == a_null -> e_neq e_zero n
+  | [_; p; n] when p == a_null -> e_lt e_zero n
   | _ -> raise Not_found
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
index b0cee81bfe10164fe4d253639781d2afa2aaa475..f07a5015c57db209d288e72590bf456f336e01a5 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -80,7 +80,7 @@ theory Memory
              ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= 1 + m[p.base] ))
 
   predicate invalid (m : map int int) (p:addr) (n:int) =
-    n > 0 -> ( m[p.base] <= p.offset \/ p.offset + n <= 0 )
+    n > 0 /\ (p = null \/ m[p.base] <= p.offset \/ p.offset + n <= 0 )
 
   lemma valid_rw_rd :
     forall m : map int int.
@@ -95,9 +95,6 @@ theory Memory
     0 <= p.offset < m[p.base] ->
     (valid_rd m p 1 /\ not (valid_rw m p 1))
 
-  lemma invalid_null :
-    forall m : map int int, n: int. n <> 0 -> invalid m null n
-
   lemma separated_1 : forall p q : addr. forall a b i j : int
     [ separated p a q b , { base = p.base ; offset = i } ,
                           { base = q.base ; offset = j } ].