diff --git a/.gitignore b/.gitignore
index f12c5c6f..2a39c64d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,2 @@
 build/*
-/.vscode/
+/.vscode/
\ No newline at end of file
diff --git a/src/example-archive/.gitignore b/src/example-archive/.gitignore
new file mode 100644
index 00000000..d863d5fb
--- /dev/null
+++ b/src/example-archive/.gitignore
@@ -0,0 +1,6 @@
+/**/coq/**/*-build/*
+/**/coq/**/*-build/theories/*
+
+!**/coq/**/*-build/
+!**/coq/**/*-build/theories/
+!**/coq/**/*-build/theories/Proofs.v
\ No newline at end of file
diff --git a/src/example-archive/README.md b/src/example-archive/README.md
index 22a7d058..24480fa3 100644
--- a/src/example-archive/README.md
+++ b/src/example-archive/README.md
@@ -10,6 +10,7 @@ This directory contains examples for CN. Each subdirectory contains examples fro
 * `Rust` - C versions of Rust programs, with CN annotations that provide the same guarantees as the Rust type-checker.
 * `SAW` - Examples derived from the [Software Analysis Workbench (SAW)](https://saw.galois.com) repository and tutorial. 
 * `open-sut` - Examples inspired by the VERSE Open System Under Test (Open SUT).
+* `coq-lemmas` - Examples with declared lemmas that can be exported to Coq for manual proofs.
 
 ## Organization  
 
@@ -25,6 +26,11 @@ are categorized according to the following schema.
 * `<source>/broken/error-proof` - examples where CN fails with error 1,
   indicating the proof failed. 
 * `<source>/broken/error-timeout` - examples where CN times out after 60s. 
+* `<source>/coq/*` - examples that CN verifies without error and have lemmas that should be extracted. According to the following rules
+    * `<source>/coq/working` - Examples where Coq lemmas can be extracted and the Coq project can be built.
+    * `<source>/coq/broken-build` - Examples where Coq lemmas can be extracted, but the Coq build process fails.
+    * `<source>/coq/broken-export` - Examples where Coq extraction fails. These should still be verifiable with CN.
+* `<source>/coq/working` - examples that CN verifies without error. 
 * `<source>/inprogress` - unfinished examples. 
 
 ## Check script
diff --git a/src/example-archive/check-all.sh b/src/example-archive/check-all.sh
index 4f712ac3..8ac928ed 100755
--- a/src/example-archive/check-all.sh
+++ b/src/example-archive/check-all.sh
@@ -2,10 +2,10 @@
 
 if [ -n "$1" ]
 then
-    echo "check-all.sh: using CN=$1 in $PWD"
-    CN="$1"
+  echo "check-all.sh: using CN=$1 in $PWD"
+  CN="$1"
 else
-    CN=cn
+  CN=cn
 fi
 
 subdirs=(
@@ -17,6 +17,7 @@ subdirs=(
   "Rust" 
   "SAW" 
   "simple-examples"
+  # "coq-lemmas"
 )
 FAILURE=0 
 
@@ -35,9 +36,9 @@ done
 
 if [ $FAILURE -eq 0 ];
 then
-    printf "\n\033[32mTest suite passes:\033[0m all CN tests in the example archive produced expected return codes\n"
-    exit 0
+  printf "\n\033[32mTest suite passes:\033[0m all CN tests in the example archive produced expected return codes\n"
+  exit 0
 else 
-    printf "\n\033[31mTest suite fails:\033[0m one or more CN tests in the example archive produced an unexpected return code\n"
-    exit 1
+  printf "\n\033[31mTest suite fails:\033[0m one or more CN tests in the example archive produced an unexpected return code\n"
+  exit 1
 fi
\ No newline at end of file
diff --git a/src/example-archive/check.sh b/src/example-archive/check.sh
index a246a369..ee1b7656 100755
--- a/src/example-archive/check.sh
+++ b/src/example-archive/check.sh
@@ -2,35 +2,33 @@
 
 if [ -n "$1" ]
 then
-    echo "check.sh: using CN=$1 in $PWD"
-    CN="$1"
+  echo "check.sh: using CN=$1 in $PWD"
+  CN="$1"
 else
-    CN=cn
+  CN=cn
 fi
 
-
-
 process_files() {
   local dir=$1
   local pattern=$2
   local action=$3
-  local expected_exit_code=$4
+  local action_argument=$4
 
   if [ -d "$dir" ]; then
-    # Array to hold files matching the pattern
-    local files=($(find "$dir" -maxdepth 1 -type f -name "$pattern" | sort))
-
-    # Check if the array is not empty
-    if [ "${#files[@]}" -gt 0 ]; then
-      for file in "${files[@]}"; do
-        # Ensure the file variable is not empty
-        if [[ -n "$file" ]]; then
-          "$action" "$file" "$expected_exit_code"
-        fi
-      done
-    else
-      echo "No files matching '$pattern' found in $dir"
+  # Array to hold files matching the pattern
+  local files=($(find "$dir" -maxdepth 1 -type f -name "$pattern" | sort))
+
+  # Check if the array is not empty
+  if [ "${#files[@]}" -gt 0 ]; then
+    for file in "${files[@]}"; do
+    # Ensure the file variable is not empty
+    if [[ -n "$file" ]]; then
+      "$action" "$file" "$action_argument"
     fi
+    done
+  else
+    echo "No files matching '$pattern' found in $dir"
+  fi
   else
     echo "Directory $dir does not exist"
   fi
@@ -38,6 +36,10 @@ process_files() {
 
 failures=0
 
+# ====================
+# Check CN verification
+# ====================
+
 check_file() {
   local file=$1
   local expected_exit_code=$2
@@ -54,11 +56,113 @@ check_file() {
   fi
 }
 
-process_files "working" "*.c" check_file 0
+printf "== Check CN verification \n"
+process_files "working" "*.c"               check_file 0
 process_files "broken/error-cerberus" "*.c" check_file 2
-process_files "broken/error-crash" "*.c" check_file 125
-process_files "broken/error-proof" "*.c" check_file 1
-process_files "broken/error-timeout" "*.c" check_file 124
+process_files "broken/error-crash" "*.c"    check_file 125
+process_files "broken/error-proof" "*.c"    check_file 1
+process_files "broken/error-timeout" "*.c"  check_file 124
+process_files "coq/broken-build" "*.c"      check_file 0
+process_files "coq/broken-export" "*.c"     check_file 0
+process_files "coq/working" "*.c"           check_file 0
+
+# ====================
+# Check Coq Exports
+# ====================
+
+
+# We allow several types of failure that can be intended
+readonly SUCCESS=0
+readonly FAIL_EXPORT=1
+readonly FAIL_COQ_BUILD=2
+
+
+check_coq_exports_end() {
+  ## Call this function at the end of a coq export check. It will
+  ## print the right message and return to the original directory
+  ## with popd. It will also increse the failure count if necessary.
+  local FAILED=$1
+  local MESSAGE=$2
+  
+  if [[ $FAILED -ne 0 ]]; then
+    printf "\033[31mFAIL\033[0m (${MESSAGE})\n"
+    failures=$(( $failures + 1 ))
+  else
+    printf "\033[32mPASS\033[0m\n"
+  fi
+}
+
+check_coq_exports() {
+  local FILE=$1
+  local FAIL_MODE=$2
+  local PROTOTYPE_BUILD_DIR="../coq-build"
+  local EXPORTED_LEMMAS="ExportedLemmas.v"
+  local result=0 #^track if the build completed as much as expected
+  
+  printf "[$FILE]... "
+  
+  # Make a copy of the build directory but only if it doesn't
+  # already exists
+  local BUILD_DIR="${FILE%.*}-build"
+
+  # Copy the build directory, and/or missing/new files
+  rsync -a "${PROTOTYPE_BUILD_DIR}/" "$BUILD_DIR"
+  
+  # Export the CN lemmas
+  $CN "--lemmata=${BUILD_DIR}/theories/${EXPORTED_LEMMAS}" $FILE > /dev/null 2>&1
+  # Check the result is as expected
+  local cn_result=$?
+  if [[ $cn_result -ne 0 && $FAIL_MODE -eq $FAIL_EXPORT ]]; then
+    # The export is expected to fail and there is nothing else to
+    # be done. Return successfully.
+    check_coq_exports_end ${result} ""
+    return ${result}
+  elif [[ $cn_result -eq 0 && $FAIL_MODE -ne $FAIL_EXPORT ]]; then
+    : # Export succeeded, as expected, continue the build
+  else
+    # Otherwise fail
+    result=1
+    check_coq_exports_end ${result} "Unexpected return code during export: $cn_result"
+    return ${result}
+  fi
+
+  # The rest of the commands must be performed in the build directory 
+  pushd "$BUILD_DIR" > /dev/null
+  
+  # Create the Coq Makefile
+  # (We don't expect this to fail)
+  coq_makefile -f _CoqProject -o Makefile.coq > /dev/null
+
+  # Build the Coq files
+  make -f Makefile.coq > /dev/null  2>&1
+  # Check the result is as expected
+  local coq_result=$?
+  if [[ $coq_result -ne 0 && $FAIL_MODE -eq $FAIL_COQ_BUILD ]]; then
+    # The coq build is expected to fail and there is nothing else to
+    # be done. Return successfully.
+    check_coq_exports_end ${result} ""
+  elif [[ $coq_result -eq 0 && $FAIL_MODE -ne $FAIL_COQ_BUILD ]]; then
+    # Export succeeded, as expected
+    check_coq_exports_end ${result} ""
+  else
+    result=1
+    check_coq_exports_end ${result} "Unexpected return code during coq build: $coq_result"
+  fi
+
+  # At this point everythink built successfully.
+
+  # Return to the directory where the script was called (from the
+  # build directory)
+  popd > /dev/null
+
+  return ${result}  
+}
+
+printf "== Check lemma export\n"
+process_files "coq/working" "*.c"       check_coq_exports $SUCCESS
+process_files "coq/broken-build" "*.c"  check_coq_exports $FAIL_COQ_BUILD
+process_files "coq/broken-export" "*.c" check_coq_exports $FAIL_EXPORT
+
 
 if [[ "$failures" = 0 ]]
 then
diff --git a/src/example-archive/coq-build/README.md b/src/example-archive/coq-build/README.md
new file mode 100644
index 00000000..7816aca6
--- /dev/null
+++ b/src/example-archive/coq-build/README.md
@@ -0,0 +1,5 @@
+## Lemma export build forlder
+
+This folder will be copied to be used as a build folder for exported lemmas. Lemmas should be extracted into the `theories/ExportedLemmas.v` and proofs, if any, should be written in `theories/Proofs.v`
+
+From the `_CoqProject` a Makefile should be generated automatically.
diff --git a/src/example-archive/coq-build/_CoqProject b/src/example-archive/coq-build/_CoqProject
new file mode 100644
index 00000000..efc08743
--- /dev/null
+++ b/src/example-archive/coq-build/_CoqProject
@@ -0,0 +1,3 @@
+-R theories CN_Lemmas
+
+theories
\ No newline at end of file
diff --git a/src/example-archive/coq-build/theories/CN_Lib.v b/src/example-archive/coq-build/theories/CN_Lib.v
new file mode 100644
index 00000000..e17d738a
--- /dev/null
+++ b/src/example-archive/coq-build/theories/CN_Lib.v
@@ -0,0 +1,29 @@
+Require List.
+Require Import ZArith Bool.
+Require Import Lia.
+Require NArith.
+
+Definition wrapI (minInt : Z) (maxInt : Z) x :=
+  let delta := ((maxInt - minInt) + 1)%Z in
+  let r := Z.modulo x delta in
+  (if (r <=? maxInt) then r else r - delta)%Z.
+
+Lemma wrapI_idem:
+  forall (minInt maxInt x : Z),
+  (minInt <= x <= maxInt)%Z ->
+  (minInt <= 0 < maxInt)%Z ->
+  wrapI minInt maxInt x = x.
+Proof.
+  Open Scope Z.
+  intros.
+  unfold wrapI.
+  pose (delta := ((maxInt - minInt) + 1)).
+  destruct (0 <=? x) eqn: x_neg.
+  - rewrite Z.mod_small by lia.
+    rewrite Zle_imp_le_bool by lia.
+    reflexivity.
+  - rewrite (Znumtheory.Zdivide_mod_minus _ _ (x + delta)).
+    + destruct (x + delta <=? maxInt) eqn: leb; lia.
+    + lia.
+    + exists (-1); lia.
+Qed.
diff --git a/src/example-archive/coq-lemmas/.gitignore b/src/example-archive/coq-lemmas/.gitignore
new file mode 100644
index 00000000..5820fc02
--- /dev/null
+++ b/src/example-archive/coq-lemmas/.gitignore
@@ -0,0 +1,9 @@
+build/**/*.vo
+build/**/*.vos
+build/**/*.vok
+build/**/*.glob
+build/**/*.aux
+Makefile.coq
+Makefile.coq.conf
+.Makefile.coq.d
+/build/.lia.cache
\ No newline at end of file
diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
new file mode 100644
index 00000000..bde0add4
--- /dev/null
+++ b/src/example-archive/coq-lemmas/README.md
@@ -0,0 +1,111 @@
+# Coq Examples
+
+CN examples using lemmas that can be extracted to Coq. The examples
+are split into:
+
+- Trivial - named `trivial-*.c`
+- Recursive - named `recursive-*.c` _(export for these examples is not supported by CN yet)_
+
+Some examples are accompanied by Coq proofs of the lemmas extracted from CN. These are stored as follows: 
+
+- Originating C file: `coq/working/EXAMPLENAME.c`
+- Coq proof: `coq/working/EXAMPLENAME-build/Proof.v` 
+
+See README in parent directory for directory organization details.
+
+## Tools needed
+
+To build the generated Coq lemmas, you will need to [download and
+install Coq](https://coq.inria.fr/download).
+
+## Batch build
+
+To export and build lemmas for all examples just run
+
+`../check.sh`. 
+
+For each file in the `coq` folder, the script first
+checks the CN verification and then exports lemmas to Coq and builds
+the Coq files. When proofs are provided, those will be built too.
+
+To provide proofs or test individual examples, see below.
+
+## Testing individual examples
+
+From this folder, to export lemmas from example `path/to/EXAMPLENAME.c`, do the following:
+
+0. (optional) Check CN verification, without exporting lemmas, with
+
+  `cn path/to/EXAMPLENAME.c`
+
+1. Create a copy of the build folder with 
+
+  `rsync -a ../coq-build/ path/to/EXAMPLENAME-build`
+  
+  (note trailing `/` after the first directory). This
+  copies a template build folder that conveniently contains a
+  `_CoqProject` file and the CN coq library `CN_Lib.v`. If the folder
+  already exists, `rsync` just updates the files.
+2. Extract the lemmas with 
+  
+  `cn --lemmata=path/to/EXAMPLENAME-build/theories/ExportedLemmas.v path/to/EXAMPLENAME.c`
+  
+  This should create a new file
+  `path/to/EXAMPLENAME-build/theories/ExportedLemmas.v` with all the
+  exported types, definitions and lemmas from the file
+  `path/to/EXAMPLENAME.c`.
+3. Go to the build directory with 
+
+  `pushd path/to/EXAMPLENAME-build`
+  
+  This will also store your current location to return later.
+4. Create or update the Coq Makefile with 
+
+  `coq_makefile -f _CoqProject -o Makefile.coq`
+  
+5. Build the Coq files with 
+
+  `make -f Makefile.coq`
+  
+  This should create `*.vo` files for every `*.v` file in the
+  `theories` directory.
+6. Return to your starting folder with 
+
+  `popd`
+
+To add proofs, after running the steps above, create a file `Proofs.v`
+in the `theories` folder, next to the generated
+`ExportedLemmas.v`. The file must contain instances of the module
+types defined in `ExportedLemmas.v`: `Parameters`, `Defs`, and
+`Lemma_Spec` module type.
+
+Your `theories/Proofs.v` file will look something like this:
+
+```
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+Require Import CN_Lemmas.ExportedLemmas.
+
+
+(*Parameters*)
+Module ConcreteParameters <:Parameters.
+(*Fill parameters here, if any*)
+End ConcreteParameters.
+
+(*Definitions*)
+Module ConcreteDefs := Defs(ConcreteParameters).
+
+Module ConcreteLemmaSpec <: Lemma_Spec(ConcreteParameters).
+  Module D := ConcreteDefs.
+  Import D.
+
+  (*Prove the lemmas, if any. *)
+  Definition example_lemma : example_lemma_type.
+  Proof. (*Add here the proof*) . Qed.
+  
+End ConcreteLemmaSpec.
+```
+
+Once all the proofs have been completed in `Proofs.v`, repeat steps
+3-6 above to build all files. If `Proofs.vo` is generated correctly,
+the extracted lemmas have been proven.
diff --git a/src/example-archive/coq-lemmas/broken/error-cerberus/trivial-005.c b/src/example-archive/coq-lemmas/broken/error-cerberus/trivial-005.c
new file mode 100644
index 00000000..13ce2e09
--- /dev/null
+++ b/src/example-archive/coq-lemmas/broken/error-cerberus/trivial-005.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_bit_wise_and (u32 x)
+  requires true;
+  ensures x & x == x;
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/broken/error-cerberus/trivial-006.c b/src/example-archive/coq-lemmas/broken/error-cerberus/trivial-006.c
new file mode 100644
index 00000000..d07ffbc2
--- /dev/null
+++ b/src/example-archive/coq-lemmas/broken/error-cerberus/trivial-006.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_bit_wise_or (u32 x)
+  requires true;
+  ensures x | x == x;
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/coq/broken-build/trivial-002-build/theories/Proofs.v b/src/example-archive/coq-lemmas/coq/broken-build/trivial-002-build/theories/Proofs.v
new file mode 100644
index 00000000..7a08e7ed
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/broken-build/trivial-002-build/theories/Proofs.v
@@ -0,0 +1,24 @@
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+Require Import CN_Lemmas.ExportedLemmas.
+
+
+(*Parameters*)
+Module ConcreteParameters <:Parameters.
+End ConcreteParameters.
+
+(*Definitions*)
+Module ConcreteDefs := Defs(ConcreteParameters).
+
+Module ConcreteLemmaSpec <: Lemma_Spec(ConcreteParameters).
+  Module D := ConcreteDefs.
+  Import D.
+
+  Definition lem_impossible_in_coq : lem_impossible_in_coq_type.
+  Proof. unfold lem_impossible_in_coq_type.
+         (* Goal: forall x : Z, x <= 4294967295*)
+         (* That's impossible to prove! *)
+  Abort. Qed.
+  
+End ConcreteLemmaSpec.
+
diff --git a/src/example-archive/coq-lemmas/coq/broken-build/trivial-004-build/theories/Proofs.v b/src/example-archive/coq-lemmas/coq/broken-build/trivial-004-build/theories/Proofs.v
new file mode 100644
index 00000000..c17457a0
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/broken-build/trivial-004-build/theories/Proofs.v
@@ -0,0 +1,27 @@
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+Require Import CN_Lemmas.ExportedLemmas.
+
+
+(*Parameters*)
+Module ConcreteParameters <:Parameters.
+End ConcreteParameters.
+
+(*Definitions*)
+Module ConcreteDefs := Defs(ConcreteParameters).
+
+Module ConcreteLemmaSpec <: Lemma_Spec(ConcreteParameters).
+  Module D := ConcreteDefs.
+  Import D.
+
+  Definition lem_impossible_in_Coq : lem_impossible_in_Coq_type.
+  Proof. unfold lem_impossible_in_Coq_type.
+         (* Goal: forall x : Z,
+            CN_Lib.wrapI 0 4294967295
+             (CN_Lib.wrapI 0 4294967295 (x + 1) - 1) = x *)
+         (* That's impossible to prove! The LHS is always in bound,
+            but x can be any Z *)
+  Abort. Qed.
+         
+End ConcreteLemmaSpec.
+
diff --git a/src/example-archive/coq-lemmas/coq/broken-export/recursive-001.c b/src/example-archive/coq-lemmas/coq/broken-export/recursive-001.c
new file mode 100644
index 00000000..b45f7289
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/broken-export/recursive-001.c
@@ -0,0 +1,40 @@
+/*@
+function [rec] (u32) fact_spec(u32 n)
+{
+  if (n <= 0u32) { 1u32 }
+  else { n * fact_spec(n - 1u32) }
+}
+@*/
+
+
+/*@
+lemma spec_lemma (u32 n)
+  requires true;
+  ensures fact_spec(n) == n * fact_spec(n-1u32);
+@*/
+
+// Function to calculate the factorial of a number
+unsigned int factorial(unsigned int n)
+/*@ requires 0u32 <= n; n <= 4294967294u32;  @*/
+/*@ requires fact_spec(n) < 4294967295u32; @*/
+/*@ ensures return == fact_spec(n); @*/
+{
+    if (n <= 0) {
+      /*@ unfold fact_spec(n); @*/
+      return 1; // Return 1
+    }
+
+    unsigned result = 1;
+    /*@ unfold fact_spec(1u32-1u32); @*/
+    for (unsigned int i = 1; i <= n; i++)
+      /*@ inv {n}unchanged; @*/
+      /*@ inv 0u32 < n; i <= n+1u32; @*/
+      /*@ inv 0u32 < i; @*/
+      /*@ inv result == fact_spec(i-1u32); @*/
+      {
+        result *= i;
+	/*@ apply spec_lemma((i+1u32)-1u32); @*/
+      }
+
+    return result;
+}
diff --git a/src/example-archive/coq-lemmas/coq/broken-export/recursive-002.c b/src/example-archive/coq-lemmas/coq/broken-export/recursive-002.c
new file mode 100644
index 00000000..d245d459
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/broken-export/recursive-002.c
@@ -0,0 +1,56 @@
+// Fails to export becasue of recursive definition
+
+/*@
+function [rec] (u32) fib_spec(u32 n)
+{
+  if (n <= 0u32) {
+    1u32
+  } else {
+    if (n == 1u32) {
+      1u32
+    } else {
+      fib_spec(n - 1u32) + fib_spec(n - 2u32)
+    }
+  }
+}
+@*/
+
+
+/*@
+lemma fib_lemma (u32 n)
+  requires true;
+  ensures fib_spec(n) == fib_spec(n - 1u32) + fib_spec(n - 2u32);
+@*/
+
+// Function to calculate the factorial of a number
+unsigned int fibonacci(unsigned int n)
+/*@ requires 0u32 <= n; n <= 4294967294u32;  @*/
+/*@ requires fib_spec(n) < 4294967295u32; @*/
+/*@ ensures return == fib_spec(n); @*/
+{
+    if (n <= 1) {
+      /*@ unfold fib_spec(n); @*/
+      return 1; // Return 1
+    }
+
+    unsigned previous = 1;
+    unsigned tmp = 1;
+    unsigned result = 1;
+    
+    /*@ unfold fib_spec(1u32-1u32); @*/
+    /*@ unfold fib_spec(1u32); @*/
+    for (unsigned int i = 1; i < n; i++)
+      /*@ inv {n}unchanged; @*/
+      /*@ inv 0u32 < n; i <= n; @*/
+      /*@ inv 0u32 < i; @*/
+      /*@ inv previous == fib_spec(i-1u32); @*/
+      /*@ inv result == fib_spec(i); @*/
+      {
+	tmp = previous;
+	previous = result;
+	result = tmp + previous;
+	/*@ apply fib_lemma(i+1u32); @*/
+      }
+
+    return result;
+}
diff --git a/src/example-archive/coq-lemmas/coq/working/trivial-001-build/theories/Proofs.v b/src/example-archive/coq-lemmas/coq/working/trivial-001-build/theories/Proofs.v
new file mode 100644
index 00000000..6101a8b4
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/working/trivial-001-build/theories/Proofs.v
@@ -0,0 +1,21 @@
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+Require Import CN_Lemmas.ExportedLemmas.
+
+
+(*Parameters*)
+Module ConcreteParameters <:Parameters.
+End ConcreteParameters.
+
+(*Definitions*)
+Module ConcreteDefs := Defs(ConcreteParameters).
+
+Module ConcreteLemmaSpec <: Lemma_Spec(ConcreteParameters).
+  Module D := ConcreteDefs.
+  Import D.
+
+  Definition lem_trivial : lem_trivial_type.
+  Proof. unfold lem_trivial_type; exact I. Qed.
+  
+End ConcreteLemmaSpec.
+
diff --git a/src/example-archive/coq-lemmas/coq/working/trivial-001.c b/src/example-archive/coq-lemmas/coq/working/trivial-001.c
new file mode 100644
index 00000000..529f1dbe
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/working/trivial-001.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_trivial ()
+  requires true;
+  ensures true; 
+@*/
+
+void lemma_1() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/coq/working/trivial-003-build/theories/Proofs.v b/src/example-archive/coq-lemmas/coq/working/trivial-003-build/theories/Proofs.v
new file mode 100644
index 00000000..91d03fc8
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/working/trivial-003-build/theories/Proofs.v
@@ -0,0 +1,23 @@
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+Require Import CN_Lemmas.ExportedLemmas.
+
+
+(*Parameters*)
+Module ConcreteParameters <:Parameters.
+End ConcreteParameters.
+
+(*Definitions*)
+Module ConcreteDefs := Defs(ConcreteParameters).
+
+Module ConcreteLemmaSpec <: Lemma_Spec(ConcreteParameters).
+  Module D := ConcreteDefs.
+  Import D.
+
+  Definition lem_ineq : lem_ineq_type.
+  Proof. unfold lem_ineq_type.
+         constructor; assumption.
+  Qed.
+  
+End ConcreteLemmaSpec.
+
diff --git a/src/example-archive/coq-lemmas/coq/working/trivial-003.c b/src/example-archive/coq-lemmas/coq/working/trivial-003.c
new file mode 100644
index 00000000..4716d24d
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/working/trivial-003.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_ineq (u32 x, u32 y)
+  requires x > 0u32; y > 0u32;
+  ensures x > 0u32; y > 0u32;
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-007.c b/src/example-archive/coq-lemmas/inprogress/trivial-007.c
new file mode 100644
index 00000000..1752d92a
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-007.c
@@ -0,0 +1,16 @@
+#include <stdbool.h>
+/*@
+  predicate (bool) MyCondition (u32 x){
+    if (x > 4294967295u32){
+      return false;
+    } else {
+      return true; 
+    }
+  } 
+
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-008.c b/src/example-archive/coq-lemmas/inprogress/trivial-008.c
new file mode 100644
index 00000000..423311ff
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-008.c
@@ -0,0 +1,11 @@
+#include <stdbool.h>
+/*@
+  lemma my_lemma ()
+  requires true;
+  ensures true;
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-009.c b/src/example-archive/coq-lemmas/inprogress/trivial-009.c
new file mode 100644
index 00000000..0583285e
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-009.c
@@ -0,0 +1,8 @@
+/*@ function [rec] (u32) my_spec(u32 n) { 42u32 } @*/
+
+unsigned int factorial(unsigned int n)
+/*@ ensures return == my_spec(n); @*/
+{
+  /*@ unfold my_spec(n); @*/
+  return 42;
+}