diff --git a/tests/fin_maps.v b/tests/fin_maps.v
index 62895b9315f45a170f321db2070404dfa2b6ee09..e8fc43ca46e7bc5896df5301e08e7e1c034099fd 100644
--- a/tests/fin_maps.v
+++ b/tests/fin_maps.v
@@ -415,12 +415,12 @@ Global Program Instance gtest_countable `{Countable K} : Countable (gtest K) :=
   inj_countable' enc dec _.
 Next Obligation.
   intros K ?? enc dec_list dec t.
-  remember (gtest_size t) as n eqn:Hn. revert t Hn.
-  induction (lt_wf n) as [n _ IH]; intros [ts] ->; simpl in *; f_equal.
+  induction (Nat.lt_wf_0_projected gtest_size t) as [[ts] _ IH].
+  simpl in *; f_equal.
   revert ts IH. apply (map_fold_ind (λ r ts, _ → dec_list dec r = ts)); [done|].
   intros i t ts r ? IHts IHt; simpl. f_equal.
-  - eapply IHt; [|done]. rewrite map_fold_insert_L by auto with lia. lia.
-  - apply IHts; intros n ? t' ->. eapply IHt; [|done].
+  - eapply IHt. rewrite map_fold_insert_L by auto with lia. lia.
+  - apply IHts; intros t' ?. eapply IHt.
     rewrite map_fold_insert_L by auto with lia. lia.
 Qed.
 
diff --git a/tests/numbers.ref b/tests/numbers.ref
index 05fcae6ea22ea896b2c8b972e9827c06356cfa13..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/tests/numbers.ref
+++ b/tests/numbers.ref
@@ -1,16 +0,0 @@
-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop
-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop
-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop
-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop
diff --git a/tests/numbers.v b/tests/numbers.v
index 0b0c6d01ccdf9c50266aff768ee7aabe9741540a..ca2376900405fa86259c3f18e1aec34d4187fb8f 100644
--- a/tests/numbers.v
+++ b/tests/numbers.v
@@ -1,26 +1,26 @@
-From stdpp Require base numbers prelude.
+From stdpp Require Import list.
 
-(** Check that we always get the [le] and [lt] functions on [nat]. *)
-Module test1.
-  Import stdpp.base.
-  Check le.
-  Check lt.
-End test1.
+(** Simple example of measure induction on lists using [Nat.lt_wf_0_projected]. *)
+Fixpoint evens {A} (l : list A) : list A :=
+  match l with
+  | x :: _ :: l => x :: evens l
+  | [x] => [x]
+  | _ => []
+  end.
 
-Module test2.
-  Import stdpp.prelude.
-  Check le.
-  Check lt.
-End test2.
+Fixpoint odds {A} (l : list A) : list A :=
+  match l with
+  | _ :: y :: l => y :: odds l
+  | _ => []
+  end.
 
-Module test3.
-  Import stdpp.numbers.
-  Check le.
-  Check lt.
-End test3.
-
-Module test4.
-  Import stdpp.list.
-  Check le.
-  Check lt.
-End test4.
+Lemma lt_wf_projected_induction_sample {A} (l : list A) :
+  evens l ++ odds l ≡ₚ l.
+Proof.
+  (** Note that we do not use [induction .. using ..]. The term
+  [Nat.lt_wf_0_projected length l] has type [Acc ..], so we perform induction
+  on the [Acc] predicate. *)
+  induction (Nat.lt_wf_0_projected length l) as [l _ IH].
+  destruct l as [|x [|y l]]; simpl; [done..|].
+  rewrite <-Permutation_middle. rewrite IH by (simpl; lia). done.
+Qed.
diff --git a/tests/numbers_import.ref b/tests/numbers_import.ref
new file mode 100644
index 0000000000000000000000000000000000000000..05fcae6ea22ea896b2c8b972e9827c06356cfa13
--- /dev/null
+++ b/tests/numbers_import.ref
@@ -0,0 +1,16 @@
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
diff --git a/tests/numbers_import.v b/tests/numbers_import.v
new file mode 100644
index 0000000000000000000000000000000000000000..0b0c6d01ccdf9c50266aff768ee7aabe9741540a
--- /dev/null
+++ b/tests/numbers_import.v
@@ -0,0 +1,26 @@
+From stdpp Require base numbers prelude.
+
+(** Check that we always get the [le] and [lt] functions on [nat]. *)
+Module test1.
+  Import stdpp.base.
+  Check le.
+  Check lt.
+End test1.
+
+Module test2.
+  Import stdpp.prelude.
+  Check le.
+  Check lt.
+End test2.
+
+Module test3.
+  Import stdpp.numbers.
+  Check le.
+  Check lt.
+End test3.
+
+Module test4.
+  Import stdpp.list.
+  Check le.
+  Check lt.
+End test4.