diff --git a/generator/tests/lambda/Lambda.v b/generator/tests/lambda/Lambda.v
index 0ea183ba9a05687c58dbe234fde4470fce9ca2d1..c29e4f48aca52ff38b146ee41c68eac31cae2ea7 100644
--- a/generator/tests/lambda/Lambda.v
+++ b/generator/tests/lambda/Lambda.v
@@ -129,8 +129,6 @@ Fixpoint run (n:nat) (t:trm) : res :=
    (otherwise, useless errors will be launched). *)
 Extraction Inline classicT LibEpsilon.Inhab_witness LibEpsilon.epsilon LibEpsilon.epsilon_def indefinite_description.
 
-Extract Constant nat_comparable => "(=)".
-
 Set Extraction AccessOpaque.
 Unset Extraction Optimize.
 Unset Extraction KeepSingleton.
diff --git a/generator/tests/lambda/LibNat.ml b/generator/tests/lambda/LibNat.ml
index 67e6cc62ae44ce7185b827490d9dd3882a639a4c..20e9a841fe6ff4834f7b42bc353167904b193008 100644
--- a/generator/tests/lambda/LibNat.ml
+++ b/generator/tests/lambda/LibNat.ml
@@ -1,7 +1,21 @@
 open Datatypes
 open LibReflect
 
+(** val nat_compare : nat -> nat -> bool **)
+
+let rec nat_compare x y =
+  match x with
+  | O ->
+    (match y with
+     | O -> Coq_true
+     | S n -> Coq_false)
+  | S x' ->
+    (match y with
+     | O -> Coq_false
+     | S y' -> nat_compare x' y')
+
 (** val nat_comparable : nat coq_Comparable **)
 
-let nat_comparable = (=)
+let nat_comparable x y =
+  nat_compare x y