diff --git a/backends/lean/Aeneas/Arith/Lemmas.lean b/backends/lean/Aeneas/Arith/Lemmas.lean
index f29f1808..15d02d54 100644
--- a/backends/lean/Aeneas/Arith/Lemmas.lean
+++ b/backends/lean/Aeneas/Arith/Lemmas.lean
@@ -11,6 +11,13 @@ theorem Int.emod_of_pos_disj (n m : Int) : m ≤ 0 ∨ (0 ≤ n % m ∧ n % m <
     . apply Int.emod_lt_of_pos; omega
   else left; omega
 
+@[nonlin_scalar_tac n / m]
+theorem Int.div_of_pos_disj (n m : Int) : n < 0 ∨ m < 0 ∨ (0 ≤ n / m ∧ n / m ≤ n) := by
+  dcases hn: 0 ≤ n <;> dcases hm: 0 ≤ m <;> try simp_all
+  right; right; constructor
+  . apply Int.ediv_nonneg <;> omega
+  . apply Int.ediv_le_self; omega
+
 theorem Int.pos_mul_pos_is_pos (n m : Int) (hm : 0 ≤ m) (hn : 0 ≤ n): 0 ≤ m * n := by
   have h : (0 : Int) = 0 * 0 := by simp
   rw [h]
@@ -29,6 +36,7 @@ section
   set_option scalarTac.nonLin true
 
   example (x y : Int) (h : 0 ≤ x ∧ 0 ≤ y) : 0 ≤ x * y := by scalar_tac
+  example (x y : Int) (h : 0 ≤ x ∧ 0 ≤ y) : 0 ≤ x / y := by scalar_tac
 
 end
 
diff --git a/backends/lean/Aeneas/ScalarTac.lean b/backends/lean/Aeneas/ScalarTac.lean
index 7d32bf44..a27abb62 100644
--- a/backends/lean/Aeneas/ScalarTac.lean
+++ b/backends/lean/Aeneas/ScalarTac.lean
@@ -1,2 +1,3 @@
 import Aeneas.ScalarTac.IntTac
 import Aeneas.ScalarTac.ScalarTac
+import Aeneas.Arith.Lemmas
diff --git a/backends/lean/Aeneas/ScalarTac/Init.lean b/backends/lean/Aeneas/ScalarTac/Init.lean
index 09c617ac..a8f8f5ed 100644
--- a/backends/lean/Aeneas/ScalarTac/Init.lean
+++ b/backends/lean/Aeneas/ScalarTac/Init.lean
@@ -16,7 +16,6 @@ namespace ScalarTac
 
 declare_aesop_rule_sets [Aeneas.ScalarTac, Aeneas.ScalarTacNonLin]
 
-#check Lean.Option.register
 register_option scalarTac.nonLin : Bool := {
   defValue := false
   group := ""
diff --git a/backends/lean/Aeneas/Std/ArraySlice.lean b/backends/lean/Aeneas/Std/ArraySlice.lean
index 49b61f84..5d5c77d9 100644
--- a/backends/lean/Aeneas/Std/ArraySlice.lean
+++ b/backends/lean/Aeneas/Std/ArraySlice.lean
@@ -607,6 +607,57 @@ def core.slice.Slice.copy_from_slice {T : Type} (_ : core.marker.Copy T)
 /- [core::array::TryFromSliceError] -/
 def core.array.TryFromSliceError := ()
 
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::get] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get {T : Type} :
+  core.ops.range.RangeFrom Usize → Slice T → Result (Option (Slice T)) := sorry
+
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::get_mut] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_mut
+  {T : Type} :
+  core.ops.range.RangeFrom Usize → Slice T → Result ((Option (Slice T)) ×
+    (Option (Slice T) → Slice T)) := sorry
+
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::get_unchecked] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_unchecked {T : Type} :
+  core.ops.range.RangeFrom Usize → ConstRawPtr (Slice T) → Result
+    (ConstRawPtr (Slice T)) := sorry
+
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::get_unchecked_mut] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_unchecked_mut {T : Type} :
+  core.ops.range.RangeFrom Usize → MutRawPtr (Slice T) → Result (MutRawPtr (Slice T)) := sorry
+
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::index] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.index {T : Type} :
+  core.ops.range.RangeFrom Usize → Slice T → Result (Slice T) := sorry
+
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::index_mut] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.index_mut {T : Type} :
+  core.ops.range.RangeFrom Usize → Slice T → Result ((Slice T) × (Slice T → Slice T)) := sorry
+
+/- Trait implementation: [core::slice::index::private_slice_index::{core::slice::index::private_slice_index::Sealed for core::ops::range::RangeFrom<usize>}] -/
+@[reducible]
+def core.slice.index.private_slice_index.SealedcoreopsrangeRangeFromUsize :
+  core.slice.index.private_slice_index.Sealed (core.ops.range.RangeFrom Usize)
+  := {}
+
+/- Trait implementation: [core::slice::index::{core::slice::index::SliceIndex<[T]> for core::ops::range::RangeFrom<usize>}] -/
+@[reducible]
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice (T : Type) :
+  core.slice.index.SliceIndex (core.ops.range.RangeFrom Usize) (Slice T) := {
+  Output := Slice T
+  sealedInst :=
+    core.slice.index.private_slice_index.SealedcoreopsrangeRangeFromUsize
+  get := core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get
+  get_mut := core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_mut
+  get_unchecked :=
+    core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_unchecked
+  get_unchecked_mut :=
+    core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_unchecked_mut
+  index := core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.index
+  index_mut :=
+    core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.index_mut
+}
+
 end Std
 
 end Aeneas
diff --git a/backends/lean/Aeneas/Std/Core.lean b/backends/lean/Aeneas/Std/Core.lean
index 4cbecb7c..ff766dbe 100644
--- a/backends/lean/Aeneas/Std/Core.lean
+++ b/backends/lean/Aeneas/Std/Core.lean
@@ -155,6 +155,11 @@ def core.result.Result.unwrap {T E : Type}
   | .Ok x => ok x
   | .Err _ => fail .panic
 
+/- [core::ops::range::RangeFrom] -/
+structure core.ops.range.RangeFrom (Idx : Type) where
+  start : Idx
+
+
 end Std
 
 end Aeneas
diff --git a/backends/lean/Aeneas/Std/Scalar.lean b/backends/lean/Aeneas/Std/Scalar.lean
index 7bbb584a..686434d9 100644
--- a/backends/lean/Aeneas/Std/Scalar.lean
+++ b/backends/lean/Aeneas/Std/Scalar.lean
@@ -89,7 +89,7 @@ def Scalar.and {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty :=
 def Scalar.or {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty :=
   sorry
 
-/- ¬ x reverst the bits of x
+/- ¬ x reverses the bits of x
 
    It has the following effect:
    - if x is unsigned, then it evaluates to Scalar.max - x
@@ -1154,10 +1154,10 @@ def int_saturating_add_in_bounds {ty} (x y : Scalar ty) :
   simp [int_saturating_add]
   split <;> constructor <;> cases ty <;> scalar_tac
 
-def Scalar.saturating_add {ty} (x y : Scalar ty) : Result (Scalar ty) :=
+def Scalar.saturating_add {ty} (x y : Scalar ty) : Scalar ty :=
   let r := int_saturating_add ty x.val y.val
   have h := int_saturating_add_in_bounds x y
-  ok ⟨ r, h.1, h.2 ⟩
+  ⟨ r, h.1, h.2 ⟩
 
 /- [core::num::{u8}::saturating_add] -/
 def core.num.U8.saturating_add := @Scalar.saturating_add ScalarTy.U8
@@ -1195,54 +1195,48 @@ def core.num.I128.saturating_add := @Scalar.saturating_add ScalarTy.I128
 /- [core::num::{isize}::saturating_add] -/
 def core.num.Isize.saturating_add := @Scalar.saturating_add ScalarTy.Isize
 
-@[pspec]
 theorem core.num.U8.saturating_add_spec (x y : U8) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > U8.max then z.val = U8.max
   else z.val = x.val + y.val
   := by
   simp [saturating_add, Scalar.saturating_add, int_saturating_add]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U16.saturating_add_spec (x y : U16) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > U16.max then z.val = U16.max
   else z.val = x.val + y.val
   := by
   simp [saturating_add, Scalar.saturating_add, int_saturating_add]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U32.saturating_add_spec (x y : U32) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > U32.max then z.val = U32.max
   else z.val = x.val + y.val
   := by
   simp [saturating_add, Scalar.saturating_add, int_saturating_add]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U64.saturating_add_spec (x y : U64) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > U64.max then z.val = U64.max
   else z.val = x.val + y.val
   := by
   simp [saturating_add, Scalar.saturating_add, int_saturating_add]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U128.saturating_add_spec (x y : U128) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > U128.max then z.val = U128.max
   else z.val = x.val + y.val
   := by
   simp [saturating_add, Scalar.saturating_add, int_saturating_add]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.Usize.saturating_add_spec (x y : Usize) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > Usize.max then z.val = Usize.max
   else z.val = x.val + y.val
   := by
@@ -1262,10 +1256,10 @@ def int_saturating_sub_in_bounds {ty} (x y : Scalar ty) :
   simp [int_saturating_sub]
   split <;> constructor <;> cases ty <;> scalar_tac
 
-def Scalar.saturating_sub {ty} (x y : Scalar ty) : Result (Scalar ty) :=
+def Scalar.saturating_sub {ty} (x y : Scalar ty) : Scalar ty :=
   let r := int_saturating_sub ty x.val y.val
   have h := int_saturating_sub_in_bounds x y
-  ok ⟨ r, h.1, h.2 ⟩
+  ⟨ r, h.1, h.2 ⟩
 
 /- [core::num::{u8}::saturating_sub] -/
 def core.num.U8.saturating_sub := @Scalar.saturating_sub ScalarTy.U8
@@ -1303,54 +1297,48 @@ def core.num.I128.saturating_sub := @Scalar.saturating_sub ScalarTy.I128
 /- [core::num::{isize}::saturating_sub] -/
 def core.num.Isize.saturating_sub := @Scalar.saturating_sub ScalarTy.Isize
 
-@[pspec]
 theorem core.num.U8.saturating_sub_spec (x y : U8) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
   simp [saturating_sub, Scalar.saturating_sub, int_saturating_sub]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U16.saturating_sub_spec (x y : U16) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
   simp [saturating_sub, Scalar.saturating_sub, int_saturating_sub]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U32.saturating_sub_spec (x y : U32) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
   simp [saturating_sub, Scalar.saturating_sub, int_saturating_sub]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U64.saturating_sub_spec (x y : U64) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
   simp [saturating_sub, Scalar.saturating_sub, int_saturating_sub]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U128.saturating_sub_spec (x y : U128) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
   simp [saturating_sub, Scalar.saturating_sub, int_saturating_sub]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.Usize.saturating_sub_spec (x y : Usize) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
@@ -1359,6 +1347,7 @@ theorem core.num.Usize.saturating_sub_spec (x y : Usize) :
 
 -- Wrapping add
 def Scalar.wrapping_add {ty} (x y : Scalar ty) : Scalar ty := sorry
+
 /- [core::num::{u8}::wrapping_add] -/
 def core.num.U8.wrapping_add := @Scalar.wrapping_add ScalarTy.U8
 
@@ -1399,6 +1388,7 @@ def core.num.Isize.wrapping_add := @Scalar.wrapping_add ScalarTy.Isize
 
 -- Wrapping sub
 def Scalar.wrapping_sub {ty} (x y : Scalar ty) : Scalar ty := sorry
+
 /- [core::num::{u8}::wrapping_sub] -/
 def core.num.U8.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U8
 
diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml
index 5fd6ee64..08a173e0 100644
--- a/src/extract/ExtractBuiltin.ml
+++ b/src/extract/ExtractBuiltin.ml
@@ -10,22 +10,6 @@ include ExtractName (* TODO: only open? *)
 
 let log = Logging.builtin_log
 
-let all_int_names =
-  [
-    "usize";
-    "u8";
-    "u16";
-    "u32";
-    "u64";
-    "u128";
-    "isize";
-    "i8";
-    "i16";
-    "i32";
-    "i64";
-    "i128";
-  ]
-
 (** Small utility to memoize some computations *)
 let mk_memoized (f : unit -> 'a) : unit -> 'a =
   let r = ref None in
@@ -133,7 +117,8 @@ type builtin_type_info = {
 
 type type_variant_kind =
   | KOpaque
-  | KStruct of (string * string) list
+  | KStruct of (string * string option) list
+      (** Contains the list of (field rust name, field extracted name) *)
   | KEnum of string list
 
 let mk_struct_constructor (type_name : string) : string =
@@ -174,6 +159,11 @@ let builtin_types () : builtin_type_info list =
             List.map
               (fun (rname, name) ->
                 ( rname,
+                  let name =
+                    match name with
+                    | None -> rname
+                    | Some name -> name
+                  in
                   match backend () with
                   | FStar | Lean -> name
                   | Coq | HOL4 -> extract_name ^ "_" ^ name ))
@@ -214,7 +204,7 @@ let builtin_types () : builtin_type_info list =
     mk_type "alloc::vec::Vec" ~keep_params:(Some [ true; false ]) ();
     (* Range *)
     mk_type "core::ops::range::Range"
-      ~kind:(KStruct [ ("start", "start"); ("end", "end_") ])
+      ~kind:(KStruct [ ("start", None); ("end", Some "end_") ])
       ();
     (* Option
 
@@ -259,6 +249,9 @@ let builtin_types () : builtin_type_info list =
         mk_type "core::result::Result" ~kind:(KEnum [ "Ok"; "Err" ]) ();
         mk_type "core::fmt::Error" ();
         mk_type "core::array::TryFromSliceError" ();
+        mk_type "core::ops::range::RangeFrom"
+          ~kind:(KStruct [ ("start", None) ])
+          ();
       ]
 
 let mk_builtin_types_map () =
@@ -551,6 +544,30 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
          mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::extend_from_slice"
            ~filter:(Some [ true; false ])
            ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::get"
+           ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::get_mut"
+           ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::get_unchecked"
+           ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::get_unchecked_mut"
+           ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::index"
+           ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::index_mut"
+           ();
        ]
       @ List.flatten
           (List.map
@@ -825,6 +842,13 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
         (* TryInto<T, U : TryFrom<T>> *)
         fmt "core::convert::{core::convert::TryInto<@T, @U>}"
           ~extract_name:(Some "core::convert::TryIntoFrom") ();
+        fmt
+          "core::slice::index::private_slice_index::Sealed<core::ops::range::RangeFrom<usize>>"
+          ();
+        fmt
+          "core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+           [@Self]>"
+          ();
       ]
   (* From<INT, bool> *)
   @ List.map
diff --git a/src/extract/ExtractName.ml b/src/extract/ExtractName.ml
index 32901248..1e88a47f 100644
--- a/src/extract/ExtractName.ml
+++ b/src/extract/ExtractName.ml
@@ -6,6 +6,25 @@ open Errors
 let log = Logging.extract_log
 let match_with_trait_decl_refs = true
 
+let all_int_names =
+  [
+    "usize";
+    "u8";
+    "u16";
+    "u32";
+    "u64";
+    "u128";
+    "isize";
+    "i8";
+    "i16";
+    "i32";
+    "i64";
+    "i128";
+  ]
+
+let literal_type_names = "bool" :: "str" :: all_int_names
+let literal_type_nameset = Collections.StringSet.of_list literal_type_names
+
 module NameMatcherMap = struct
   module NMM = NameMatcherMap
 
@@ -44,16 +63,18 @@ let pattern_to_extract_name (span : Meta.span option) (name : pattern) :
     List.for_all check
   in
 
-  (* This is a bit of a hack: we want to simplify the occurrences of
-     tuples of two variables, arrays with only variables, slices with
-     only variables, etc.
+  (* This is a bit of a hack: we want to simplify some names.
      We explore the pattern and replace such occurrences with a specific name.
   *)
-  let replace_option_name (id : pattern) =
+  let simplify_name (id : pattern) =
     match id with
     | [ PIdent ("core", []); PIdent ("option", []); PIdent ("Option", g) ] ->
         (* Option *)
         [ PIdent ("Option", g) ]
+    | [ PIdent (id, []) ] when Collections.StringSet.mem id literal_type_nameset
+      ->
+        (* Literals: we want to capitalize the first letter *)
+        [ PIdent (StringUtils.capitalize_first_letter id, []) ]
     | _ -> id
   in
   let visitor =
@@ -66,7 +87,7 @@ let pattern_to_extract_name (span : Meta.span option) (name : pattern) :
 
       method! visit_EComp _ id =
         (* Simplify if this is [Option] *)
-        super#visit_EComp () (replace_option_name id)
+        super#visit_EComp () (simplify_name id)
 
       method! visit_PImpl _ ty =
         match ty with
diff --git a/src/extract/ExtractTypes.ml b/src/extract/ExtractTypes.ml
index 8b6a7369..8874113c 100644
--- a/src/extract/ExtractTypes.ml
+++ b/src/extract/ExtractTypes.ml
@@ -234,11 +234,11 @@ let extract_binop (span : Meta.span)
         | FStar | Lean | HOL4 -> binop
         | Coq -> "s" ^ binop
       in
-      extract_expr false arg0;
+      extract_expr true arg0;
       F.pp_print_space fmt ();
       F.pp_print_string fmt binop;
       F.pp_print_space fmt ();
-      extract_expr false arg1
+      extract_expr true arg1
   | _ ->
       let binop_is_shift =
         match binop with
diff --git a/tests/lean/Scalars.lean b/tests/lean/Scalars.lean
index 03601f9c..57f426f5 100644
--- a/tests/lean/Scalars.lean
+++ b/tests/lean/Scalars.lean
@@ -48,23 +48,28 @@ def u32_use_shift_left (x : U32) : Result U32 :=
 def i32_use_shift_left (x : I32) : Result I32 :=
   x <<< 2#i32
 
-/- [scalars::u32_use_rotate_right]:
+/- [scalars::add_and]:
    Source: 'tests/src/scalars.rs', lines 35:0-37:1 -/
+def add_and (a : U32) (b : U32) : Result U32 :=
+  (b &&& a) + (b &&& a)
+
+/- [scalars::u32_use_rotate_right]:
+   Source: 'tests/src/scalars.rs', lines 39:0-41:1 -/
 def u32_use_rotate_right (x : U32) : Result U32 :=
   Result.ok (core.num.U32.rotate_right x 2#u32)
 
 /- [scalars::i32_use_rotate_right]:
-   Source: 'tests/src/scalars.rs', lines 39:0-41:1 -/
+   Source: 'tests/src/scalars.rs', lines 43:0-45:1 -/
 def i32_use_rotate_right (x : I32) : Result I32 :=
   Result.ok (core.num.I32.rotate_right x 2#u32)
 
 /- [scalars::u32_use_rotate_left]:
-   Source: 'tests/src/scalars.rs', lines 43:0-45:1 -/
+   Source: 'tests/src/scalars.rs', lines 47:0-49:1 -/
 def u32_use_rotate_left (x : U32) : Result U32 :=
   Result.ok (core.num.U32.rotate_left x 2#u32)
 
 /- [scalars::i32_use_rotate_left]:
-   Source: 'tests/src/scalars.rs', lines 47:0-49:1 -/
+   Source: 'tests/src/scalars.rs', lines 51:0-53:1 -/
 def i32_use_rotate_left (x : I32) : Result I32 :=
   Result.ok (core.num.I32.rotate_left x 2#u32)
 
diff --git a/tests/lean/Slices.lean b/tests/lean/Slices.lean
new file mode 100644
index 00000000..7e622052
--- /dev/null
+++ b/tests/lean/Slices.lean
@@ -0,0 +1,26 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [slices]
+import Aeneas
+open Aeneas.Std
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace slices
+
+/- [slices::slice_subslice_from_shared]:
+   Source: 'tests/src/slices.rs', lines 3:0-5:1 -/
+def slice_subslice_from_shared (x : Slice U32) : Result (Slice U32) :=
+  core.slice.index.Slice.index
+    (core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice U32) x
+    { start := 0#usize }
+
+/- [slices::slice_subslice_from_mut]:
+   Source: 'tests/src/slices.rs', lines 7:0-9:1 -/
+def slice_subslice_from_mut
+  (x : Slice U32) : Result ((Slice U32) × (Slice U32 → Slice U32)) :=
+  core.slice.index.Slice.index_mut
+    (core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice U32) x
+    { start := 0#usize }
+
+end slices
diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean
index ec8ed987..78f199f8 100644
--- a/tests/lean/lakefile.lean
+++ b/tests/lean/lakefile.lean
@@ -1,9 +1,6 @@
 import Lake
 open Lake DSL
 
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"
-
 require aeneas from "../../backends/lean"
 
 package «tests» {}
diff --git a/tests/src/scalars.rs b/tests/src/scalars.rs
index 892994f5..f3d1f19f 100644
--- a/tests/src/scalars.rs
+++ b/tests/src/scalars.rs
@@ -32,6 +32,10 @@ fn i32_use_shift_left(x: i32) -> i32 {
     x << 2
 }
 
+fn add_and(a: u32, b: u32) -> u32 {
+    (b & a) + (b & a)
+}
+
 fn u32_use_rotate_right(x: u32) -> u32 {
     x.rotate_right(2)
 }
diff --git a/tests/src/slices.rs b/tests/src/slices.rs
new file mode 100644
index 00000000..ee9af342
--- /dev/null
+++ b/tests/src/slices.rs
@@ -0,0 +1,9 @@
+//@ [coq,fstar,borrow-check] skip
+
+pub fn slice_subslice_from_shared(x: &[u32]) -> &[u32] {
+    &x[0..]
+}
+
+pub fn slice_subslice_from_mut(x: &mut [u32]) -> &mut [u32] {
+    &mut x[0..]
+}