1 files changed, 8 insertions, 0 deletions
diff --git a/common/Memdata.v b/common/Memdata.v
index 1bd87169..c80b3754 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -24,6 +24,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
+Require Import Lia.
 
 (** * Properties of memory chunks *)
 
@@ -45,6 +46,13 @@ Definition size_chunk (chunk: memory_chunk) : Z :=
   | Many64 => 8
   end.
 
+Definition largest_size_chunk := 8.
+
+Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
+Proof.
+  destruct chunk; simpl; lia.
+Qed.
+
 Lemma size_chunk_pos:
   forall chunk, size_chunk chunk > 0.
 Proof.