diff --git a/creusot-contracts/src/std/cmp.rs b/creusot-contracts/src/std/cmp.rs
index 9db3799cce..0c568460d2 100644
--- a/creusot-contracts/src/std/cmp.rs
+++ b/creusot-contracts/src/std/cmp.rs
@@ -18,7 +18,9 @@ extern_spec! {
                 fn ne(&self, rhs: &Rhs) -> bool
                 where
                     Self: DeepModel,
-                    Rhs: DeepModel<DeepModelTy = Self::DeepModelTy>;
+                    Rhs: DeepModel<DeepModelTy = Self::DeepModelTy> {
+                    !(self == rhs)
+                }
             }
 
             // TODO: for now, we only support total orders
@@ -31,16 +33,36 @@ extern_spec! {
                 fn partial_cmp(&self, rhs: &Rhs) -> Option<Ordering>;
 
                 #[ensures(result == (self.deep_model() < other.deep_model()))]
-                fn lt(&self, other: &Rhs) -> bool;
+                fn lt(&self, other: &Rhs) -> bool {
+                    match self.partial_cmp(other) {
+                        Some(Ordering::Less) => true,
+                        _ => false,
+                    }
+                }
 
                 #[ensures(result == (self.deep_model() <= other.deep_model()))]
-                fn le(&self, other: &Rhs) -> bool;
+                fn le(&self, other: &Rhs) -> bool {
+                    match self.partial_cmp(other) {
+                        Some(Ordering::Less | Ordering::Equal) => true,
+                        _ => false,
+                    }
+                }
 
                 #[ensures(result == (self.deep_model() > other.deep_model()))]
-                fn gt(&self, other: &Rhs) -> bool;
+                fn gt(&self, other: &Rhs) -> bool {
+                    match self.partial_cmp(other) {
+                        Some(Ordering::Greater) => true,
+                        _ => false,
+                    }
+                }
 
                 #[ensures(result == (self.deep_model() >= other.deep_model()))]
-                fn ge(&self, other: &Rhs) -> bool;
+                fn ge(&self, other: &Rhs) -> bool {
+                    match self.partial_cmp(other) {
+                        Some(Ordering::Greater | Ordering::Equal) => true,
+                        _ => false,
+                    }
+                }
             }
 
             trait Ord
@@ -55,7 +77,53 @@ extern_spec! {
                 #[ensures(result == self || result == o)]
                 #[ensures(self.deep_model() <= o.deep_model() ==> result == o)]
                 #[ensures(o.deep_model() < self.deep_model() ==> result == self)]
-                fn max(self, o: Self) -> Self;
+                fn max(self, o: Self) -> Self {
+                    if self <= o { o } else { self }
+                }
+
+                #[ensures(result.deep_model() <= self.deep_model())]
+                #[ensures(result.deep_model() <= o.deep_model())]
+                #[ensures(result == self || result == o)]
+                #[ensures(self.deep_model() < o.deep_model() ==> result == self)]
+                #[ensures(o.deep_model() <= self.deep_model() ==> result == o)]
+                fn min(self, o: Self) -> Self {
+                    if self < o { self } else { o }
+                }
+
+                #[requires(min.deep_model() <= max.deep_model())]
+                #[ensures(result.deep_model() >= min.deep_model())]
+                #[ensures(result.deep_model() <= max.deep_model())]
+                #[ensures(result == self || result == min || result == max)]
+                #[ensures(if self.deep_model() > max.deep_model() {
+                    result == max
+                } else if self.deep_model() < min.deep_model() {
+                    result == min
+                } else { result == self })]
+                fn clamp(self, min: Self, max: Self) -> Self {
+                    if self > max { max } else if self < min { min } else { self }
+                }
+            }
+
+            #[ensures(result.deep_model() >= v1.deep_model())]
+            #[ensures(result.deep_model() >= v2.deep_model())]
+            #[ensures(result == v1 || result == v2)]
+            #[ensures(v1.deep_model() <= v2.deep_model() ==> result == v2)]
+            #[ensures(v2.deep_model() < v1.deep_model() ==> result == v1)]
+            fn max<T>(v1: T, v2: T) -> T
+                where T: Ord + DeepModel, T::DeepModelTy: OrdLogic
+            {
+                <T as Ord>::max(v1, v2)
+            }
+
+            #[ensures(result.deep_model() <= v1.deep_model())]
+            #[ensures(result.deep_model() <= v2.deep_model())]
+            #[ensures(result == v1 || result == v2)]
+            #[ensures(v1.deep_model() < v2.deep_model() ==> result == v1)]
+            #[ensures(v2.deep_model() <= v1.deep_model() ==> result == v2)]
+            fn min<T>(v1: T, v2: T) -> T
+                where T: Ord + DeepModel, T::DeepModelTy: OrdLogic
+            {
+                <T as Ord>::min(v1, v2)
             }
         }
     }
diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma
index 95709096a5..cfbca1ad4e 100644
--- a/creusot/tests/creusot-contracts/creusot-contracts.coma
+++ b/creusot/tests/creusot-contracts/creusot-contracts.coma
@@ -92,11 +92,1618 @@ module M_creusot_contracts__stdqy35z1__array__qyi15505960269205342033__produces_
   goal vc_produces_trans'0 : ([%#sarray1] produces'0 b bc c)
    -> ([%#sarray0] produces'0 a ab b)  -> ([%#sarray2] produces'0 a (Seq.(++) ab bc) c)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log [#"../../../creusot-contracts/src/std/cmp.rs" 88 4 88 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 87 14 87 64
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 85 4 85 10
+module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_PartialEq_Rhs_ne_body [#"../../../creusot-contracts/src/std/cmp.rs" 10 31 18 18]
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 18 29 18 32
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 17 26 17 75
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 11 26 11 75
+  let%span smodel4 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
+  let%span sinvariant5 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  
+  use prelude.prelude.Borrow
+  
+  type t_Self_'0
+  
+  predicate inv'4 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Self_'0) =
+    [%#sinvariant5] inv'4 self
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_Self_'0 [inv'0 x] . inv'0 x = invariant'0 x
+  
+  predicate invariant'2 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Self_'0) =
+    [%#sinvariant5] inv'0 self
+  
+  predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  axiom inv_axiom'2 [@rewrite] : forall x : t_Self_'0 [inv'2 x] . inv'2 x = invariant'2 x
+  
+  type t_Rhs'0
+  
+  predicate inv'5 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Rhs'0)
+  
+  predicate invariant'1 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Rhs'0) =
+    [%#sinvariant5] inv'5 self
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Rhs'0)
+  
+  axiom inv_axiom'1 [@rewrite] : forall x : t_Rhs'0 [inv'1 x] . inv'1 x = invariant'1 x
+  
+  predicate invariant'3 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Rhs'0) =
+    [%#sinvariant5] inv'1 self
+  
+  predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Rhs'0)
+  
+  axiom inv_axiom'3 [@rewrite] : forall x : t_Rhs'0 [inv'3 x] . inv'3 x = invariant'3 x
+  
+  type t_DeepModelTy'0
+  
+  function deep_model'4 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Self_'0) : t_DeepModelTy'0
+  
+  function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Self_'0) : t_DeepModelTy'0 =
+    [%#smodel4] deep_model'4 self
+  
+  function deep_model'2 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Self_'0) : t_DeepModelTy'0 =
+    [%#smodel4] deep_model'0 self
+  
+  function deep_model'5 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Rhs'0) : t_DeepModelTy'0
+  
+  function deep_model'1 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Rhs'0) : t_DeepModelTy'0 =
+    [%#smodel4] deep_model'5 self
+  
+  function deep_model'3 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Rhs'0) : t_DeepModelTy'0 =
+    [%#smodel4] deep_model'1 self
+  
+  let rec eq'0 (self:t_Self_'0) (other:t_Rhs'0) (return'  (ret:bool))= {[@expl:eq 'self' type invariant] inv'2 self}
+    {[@expl:eq 'other' type invariant] inv'3 other}
+    any [ return' (result:bool)-> {[%#scmp3] result = (deep_model'2 self = deep_model'3 other)} (! return' {result}) ] 
+  
+  use prelude.prelude.Intrinsic
+  
+  meta "compute_max_steps" 1000000
+  
+  let rec extern_spec_std_cmp_PartialEq_Rhs_ne_body'0 (self_:t_Self_'0) (rhs:t_Rhs'0) (return'  (ret:bool))= {[@expl:extern_spec_std_cmp_PartialEq_Rhs_ne_body 'self_' type invariant] [%#scmp0] inv'0 self_}
+    {[@expl:extern_spec_std_cmp_PartialEq_Rhs_ne_body 'rhs' type invariant] [%#scmp1] inv'1 rhs}
+    (! bb0
+    [ bb0 = s0 [ s0 = eq'0 {self_} {rhs} (fun (_ret':bool) ->  [ &_4 <- _ret' ] s1) | s1 = bb1 ] 
+    | bb1 = s0 [ s0 =  [ &_0 <- not _4 ] s1 | s1 = return' {_0} ]  ]
+    ) [ & _0 : bool = any_l () | & self_ : t_Self_'0 = self_ | & rhs : t_Rhs'0 = rhs | & _4 : bool = any_l () ] 
+    [ return' (result:bool)-> {[@expl:extern_spec_std_cmp_PartialEq_Rhs_ne_body ensures] [%#scmp2] result
+      = (deep_model'0 self_ <> deep_model'1 rhs)}
+      (! return' {result}) ]
+    
+end
+module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_PartialOrd_Rhs_lt_body [#"../../../creusot-contracts/src/std/cmp.rs" 27 32 36 18]
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 39 29 39 34
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 38 48 38 52
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 36 29 36 34
+  let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 35 26 35 76
+  let%span scmp5 = "../../../creusot-contracts/src/std/cmp.rs" 32 26 32 91
+  let%span smodel6 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
+  let%span sord7 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
+  let%span sord8 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
+  let%span sord9 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
+  let%span sord10 = "../../../creusot-contracts/src/logic/ord.rs" 62 14 62 64
+  let%span sord11 = "../../../creusot-contracts/src/logic/ord.rs" 67 14 67 45
+  let%span sord12 = "../../../creusot-contracts/src/logic/ord.rs" 72 15 72 32
+  let%span sord13 = "../../../creusot-contracts/src/logic/ord.rs" 73 15 73 32
+  let%span sord14 = "../../../creusot-contracts/src/logic/ord.rs" 74 14 74 31
+  let%span sord15 = "../../../creusot-contracts/src/logic/ord.rs" 81 15 81 45
+  let%span sord16 = "../../../creusot-contracts/src/logic/ord.rs" 82 14 82 47
+  let%span sord17 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48
+  let%span sord18 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44
+  let%span sord19 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59
+  let%span sinvariant20 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  
+  use prelude.prelude.Borrow
+  
+  type t_Self_'0
+  
+  predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Self_'0) =
+    [%#sinvariant20] inv'2 self
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_Self_'0 [inv'0 x] . inv'0 x = invariant'0 x
+  
+  type t_Rhs'0
+  
+  predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Rhs'0)
+  
+  predicate invariant'1 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Rhs'0) =
+    [%#sinvariant20] inv'3 self
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Rhs'0)
+  
+  axiom inv_axiom'1 [@rewrite] : forall x : t_Rhs'0 [inv'1 x] . inv'1 x = invariant'1 x
+  
+  type t_DeepModelTy'0
+  
+  function deep_model'2 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Self_'0) : t_DeepModelTy'0
+  
+  function deep_model'3 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Rhs'0) : t_DeepModelTy'0
+  
+  type t_Ordering'0  =
+    | C_Less'0
+    | C_Equal'0
+    | C_Greater'0
+  
+  function cmp_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 19 4 19 46] (self : t_DeepModelTy'0) (other : t_DeepModelTy'0) : t_Ordering'0
+    
+  
+  function eq_cmp'0 [#"../../../creusot-contracts/src/logic/ord.rs" 96 4 96 32] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom eq_cmp'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord19] (x = y)
+  = (cmp_log'0 x y = C_Equal'0)
+  
+  function antisym2'0 [#"../../../creusot-contracts/src/logic/ord.rs" 91 4 91 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym2'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord17] cmp_log'0 x y = C_Greater'0)
+   -> ([%#sord18] cmp_log'0 y x = C_Less'0)
+  
+  function antisym1'0 [#"../../../creusot-contracts/src/logic/ord.rs" 83 4 83 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym1'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord15] cmp_log'0 x y = C_Less'0)
+   -> ([%#sord16] cmp_log'0 y x = C_Greater'0)
+  
+  function trans'0 [#"../../../creusot-contracts/src/logic/ord.rs" 75 4 75 53] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) (z : t_DeepModelTy'0) (o : t_Ordering'0) : ()
+    
+  
+  axiom trans'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0, z : t_DeepModelTy'0, o : t_Ordering'0 . ([%#sord12] cmp_log'0 x y
+  = o)  -> ([%#sord13] cmp_log'0 y z = o)  -> ([%#sord14] cmp_log'0 x z = o)
+  
+  function refl'0 [#"../../../creusot-contracts/src/logic/ord.rs" 68 4 68 21] (x : t_DeepModelTy'0) : ()
+  
+  axiom refl'0_spec : forall x : t_DeepModelTy'0 . [%#sord11] cmp_log'0 x x = C_Equal'0
+  
+  function gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 57 4 57 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 63 4 63 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_gt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord10] gt_log'0 x y
+  = (cmp_log'0 x y = C_Greater'0)
+  
+  function ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 46 4 46 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 52 4 52 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_ge_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord9] ge_log'0 x y
+  = (cmp_log'0 x y <> C_Less'0)
+  
+  function lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 35 4 35 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 41 4 41 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_lt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord8] lt_log'0 x y
+  = (cmp_log'0 x y = C_Less'0)
+  
+  function le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 24 4 24 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 30 4 30 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_le_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord7] le_log'0 x y
+  = (cmp_log'0 x y <> C_Greater'0)
+  
+  type t_Option'0  =
+    | C_None'0
+    | C_Some'0 (t_Ordering'0)
+  
+  let rec partial_cmp'0 (self:t_Self_'0) (other:t_Rhs'0) (return'  (ret:t_Option'0))= {[@expl:partial_cmp 'self' type invariant] inv'0 self}
+    {[@expl:partial_cmp 'other' type invariant] inv'1 other}
+    any
+    [ return' (result:t_Option'0)-> {[%#scmp5] result = C_Some'0 (cmp_log'0 (deep_model'2 self) (deep_model'3 other))}
+      (! return' {result}) ]
+    
+  
+  let rec v_Some'0 (input:t_Option'0) (ret  (field_0:t_Ordering'0))= any
+    [ good (field_0:t_Ordering'0)-> {C_Some'0 field_0 = input} (! ret {field_0})
+    | bad -> {forall field_0 : t_Ordering'0 [C_Some'0 field_0 : t_Option'0] . C_Some'0 field_0 <> input}
+      (! {false}
+      any) ]
+    
+  
+  use prelude.prelude.Intrinsic
+  
+  function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Self_'0) : t_DeepModelTy'0 =
+    [%#smodel6] deep_model'2 self
+  
+  function deep_model'1 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Rhs'0) : t_DeepModelTy'0 =
+    [%#smodel6] deep_model'3 self
+  
+  meta "compute_max_steps" 1000000
+  
+  let rec extern_spec_std_cmp_PartialOrd_Rhs_lt_body'0 (self_:t_Self_'0) (other:t_Rhs'0) (return'  (ret:bool))= {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_lt_body 'self_' type invariant] [%#scmp2] inv'0 self_}
+    {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_lt_body 'other' type invariant] [%#scmp3] inv'1 other}
+    (! bb0
+    [ bb0 = s0 [ s0 = partial_cmp'0 {self_} {other} (fun (_ret':t_Option'0) ->  [ &_4 <- _ret' ] s1) | s1 = bb1 ] 
+    | bb1 = any [ br0 -> {_4 = C_None'0 } (! bb8) | br1 (x0:t_Ordering'0)-> {_4 = C_Some'0 x0} (! bb3) ] 
+    | bb8 = bb2
+    | bb3 = v_Some'0 {_4}
+        (fun (r0'0:t_Ordering'0) ->
+          any
+          [ br0 -> {r0'0 = C_Less'0 } (! bb4)
+          | br1 -> {r0'0 = C_Equal'0 } (! bb2)
+          | br2 -> {r0'0 = C_Greater'0 } (! bb2) ]
+          )
+    | bb2 = s0 [ s0 =  [ &_0 <- [%#scmp0] false ] s1 | s1 = bb6 ] 
+    | bb4 = bb5
+    | bb5 = s0 [ s0 =  [ &_0 <- [%#scmp1] true ] s1 | s1 = bb6 ] 
+    | bb6 = return' {_0} ]
+    )
+    [ & _0 : bool = any_l () | & self_ : t_Self_'0 = self_ | & other : t_Rhs'0 = other | & _4 : t_Option'0 = any_l () ]
+    
+    [ return' (result:bool)-> {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_lt_body ensures] [%#scmp4] result
+      = lt_log'0 (deep_model'0 self_) (deep_model'1 other)}
+      (! return' {result}) ]
+    
+end
+module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_PartialOrd_Rhs_le_body [#"../../../creusot-contracts/src/std/cmp.rs" 27 32 44 18]
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 47 29 47 34
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 46 66 46 70
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 44 29 44 34
+  let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 43 26 43 77
+  let%span scmp5 = "../../../creusot-contracts/src/std/cmp.rs" 32 26 32 91
+  let%span smodel6 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
+  let%span sord7 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
+  let%span sord8 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
+  let%span sord9 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
+  let%span sord10 = "../../../creusot-contracts/src/logic/ord.rs" 62 14 62 64
+  let%span sord11 = "../../../creusot-contracts/src/logic/ord.rs" 67 14 67 45
+  let%span sord12 = "../../../creusot-contracts/src/logic/ord.rs" 72 15 72 32
+  let%span sord13 = "../../../creusot-contracts/src/logic/ord.rs" 73 15 73 32
+  let%span sord14 = "../../../creusot-contracts/src/logic/ord.rs" 74 14 74 31
+  let%span sord15 = "../../../creusot-contracts/src/logic/ord.rs" 81 15 81 45
+  let%span sord16 = "../../../creusot-contracts/src/logic/ord.rs" 82 14 82 47
+  let%span sord17 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48
+  let%span sord18 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44
+  let%span sord19 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59
+  let%span sinvariant20 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  
+  use prelude.prelude.Borrow
+  
+  type t_Self_'0
+  
+  predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Self_'0) =
+    [%#sinvariant20] inv'2 self
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_Self_'0 [inv'0 x] . inv'0 x = invariant'0 x
+  
+  type t_Rhs'0
+  
+  predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Rhs'0)
+  
+  predicate invariant'1 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Rhs'0) =
+    [%#sinvariant20] inv'3 self
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Rhs'0)
+  
+  axiom inv_axiom'1 [@rewrite] : forall x : t_Rhs'0 [inv'1 x] . inv'1 x = invariant'1 x
+  
+  type t_DeepModelTy'0
+  
+  function deep_model'2 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Self_'0) : t_DeepModelTy'0
+  
+  function deep_model'3 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Rhs'0) : t_DeepModelTy'0
+  
+  type t_Ordering'0  =
+    | C_Less'0
+    | C_Equal'0
+    | C_Greater'0
+  
+  function cmp_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 19 4 19 46] (self : t_DeepModelTy'0) (other : t_DeepModelTy'0) : t_Ordering'0
+    
+  
+  function eq_cmp'0 [#"../../../creusot-contracts/src/logic/ord.rs" 96 4 96 32] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom eq_cmp'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord19] (x = y)
+  = (cmp_log'0 x y = C_Equal'0)
+  
+  function antisym2'0 [#"../../../creusot-contracts/src/logic/ord.rs" 91 4 91 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym2'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord17] cmp_log'0 x y = C_Greater'0)
+   -> ([%#sord18] cmp_log'0 y x = C_Less'0)
+  
+  function antisym1'0 [#"../../../creusot-contracts/src/logic/ord.rs" 83 4 83 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym1'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord15] cmp_log'0 x y = C_Less'0)
+   -> ([%#sord16] cmp_log'0 y x = C_Greater'0)
+  
+  function trans'0 [#"../../../creusot-contracts/src/logic/ord.rs" 75 4 75 53] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) (z : t_DeepModelTy'0) (o : t_Ordering'0) : ()
+    
+  
+  axiom trans'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0, z : t_DeepModelTy'0, o : t_Ordering'0 . ([%#sord12] cmp_log'0 x y
+  = o)  -> ([%#sord13] cmp_log'0 y z = o)  -> ([%#sord14] cmp_log'0 x z = o)
+  
+  function refl'0 [#"../../../creusot-contracts/src/logic/ord.rs" 68 4 68 21] (x : t_DeepModelTy'0) : ()
+  
+  axiom refl'0_spec : forall x : t_DeepModelTy'0 . [%#sord11] cmp_log'0 x x = C_Equal'0
+  
+  function gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 57 4 57 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 63 4 63 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_gt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord10] gt_log'0 x y
+  = (cmp_log'0 x y = C_Greater'0)
+  
+  function ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 46 4 46 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 52 4 52 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_ge_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord9] ge_log'0 x y
+  = (cmp_log'0 x y <> C_Less'0)
+  
+  function lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 35 4 35 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 41 4 41 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_lt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord8] lt_log'0 x y
+  = (cmp_log'0 x y = C_Less'0)
+  
+  function le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 24 4 24 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 30 4 30 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_le_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord7] le_log'0 x y
+  = (cmp_log'0 x y <> C_Greater'0)
+  
+  type t_Option'0  =
+    | C_None'0
+    | C_Some'0 (t_Ordering'0)
+  
+  let rec partial_cmp'0 (self:t_Self_'0) (other:t_Rhs'0) (return'  (ret:t_Option'0))= {[@expl:partial_cmp 'self' type invariant] inv'0 self}
+    {[@expl:partial_cmp 'other' type invariant] inv'1 other}
+    any
+    [ return' (result:t_Option'0)-> {[%#scmp5] result = C_Some'0 (cmp_log'0 (deep_model'2 self) (deep_model'3 other))}
+      (! return' {result}) ]
+    
+  
+  let rec v_Some'0 (input:t_Option'0) (ret  (field_0:t_Ordering'0))= any
+    [ good (field_0:t_Ordering'0)-> {C_Some'0 field_0 = input} (! ret {field_0})
+    | bad -> {forall field_0 : t_Ordering'0 [C_Some'0 field_0 : t_Option'0] . C_Some'0 field_0 <> input}
+      (! {false}
+      any) ]
+    
+  
+  use prelude.prelude.Intrinsic
+  
+  function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Self_'0) : t_DeepModelTy'0 =
+    [%#smodel6] deep_model'2 self
+  
+  function deep_model'1 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Rhs'0) : t_DeepModelTy'0 =
+    [%#smodel6] deep_model'3 self
+  
+  meta "compute_max_steps" 1000000
+  
+  let rec extern_spec_std_cmp_PartialOrd_Rhs_le_body'0 (self_:t_Self_'0) (other:t_Rhs'0) (return'  (ret:bool))= {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_le_body 'self_' type invariant] [%#scmp2] inv'0 self_}
+    {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_le_body 'other' type invariant] [%#scmp3] inv'1 other}
+    (! bb0
+    [ bb0 = s0 [ s0 = partial_cmp'0 {self_} {other} (fun (_ret':t_Option'0) ->  [ &_4 <- _ret' ] s1) | s1 = bb1 ] 
+    | bb1 = any [ br0 -> {_4 = C_None'0 } (! bb8) | br1 (x0:t_Ordering'0)-> {_4 = C_Some'0 x0} (! bb3) ] 
+    | bb8 = bb2
+    | bb3 = v_Some'0 {_4}
+        (fun (r0'0:t_Ordering'0) ->
+          any
+          [ br0 -> {r0'0 = C_Less'0 } (! bb4)
+          | br1 -> {r0'0 = C_Equal'0 } (! bb4)
+          | br2 -> {r0'0 = C_Greater'0 } (! bb2) ]
+          )
+    | bb2 = s0 [ s0 =  [ &_0 <- [%#scmp0] false ] s1 | s1 = bb6 ] 
+    | bb4 = bb5
+    | bb5 = s0 [ s0 =  [ &_0 <- [%#scmp1] true ] s1 | s1 = bb6 ] 
+    | bb6 = return' {_0} ]
+    )
+    [ & _0 : bool = any_l () | & self_ : t_Self_'0 = self_ | & other : t_Rhs'0 = other | & _4 : t_Option'0 = any_l () ]
+    
+    [ return' (result:bool)-> {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_le_body ensures] [%#scmp4] result
+      = le_log'0 (deep_model'0 self_) (deep_model'1 other)}
+      (! return' {result}) ]
+    
+end
+module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_PartialOrd_Rhs_gt_body [#"../../../creusot-contracts/src/std/cmp.rs" 27 32 52 18]
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 55 29 55 34
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 54 51 54 55
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 52 29 52 34
+  let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 51 26 51 76
+  let%span scmp5 = "../../../creusot-contracts/src/std/cmp.rs" 32 26 32 91
+  let%span smodel6 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
+  let%span sord7 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
+  let%span sord8 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
+  let%span sord9 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
+  let%span sord10 = "../../../creusot-contracts/src/logic/ord.rs" 62 14 62 64
+  let%span sord11 = "../../../creusot-contracts/src/logic/ord.rs" 67 14 67 45
+  let%span sord12 = "../../../creusot-contracts/src/logic/ord.rs" 72 15 72 32
+  let%span sord13 = "../../../creusot-contracts/src/logic/ord.rs" 73 15 73 32
+  let%span sord14 = "../../../creusot-contracts/src/logic/ord.rs" 74 14 74 31
+  let%span sord15 = "../../../creusot-contracts/src/logic/ord.rs" 81 15 81 45
+  let%span sord16 = "../../../creusot-contracts/src/logic/ord.rs" 82 14 82 47
+  let%span sord17 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48
+  let%span sord18 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44
+  let%span sord19 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59
+  let%span sinvariant20 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  
+  use prelude.prelude.Borrow
+  
+  type t_Self_'0
+  
+  predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Self_'0) =
+    [%#sinvariant20] inv'2 self
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_Self_'0 [inv'0 x] . inv'0 x = invariant'0 x
+  
+  type t_Rhs'0
+  
+  predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Rhs'0)
+  
+  predicate invariant'1 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Rhs'0) =
+    [%#sinvariant20] inv'3 self
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Rhs'0)
+  
+  axiom inv_axiom'1 [@rewrite] : forall x : t_Rhs'0 [inv'1 x] . inv'1 x = invariant'1 x
+  
+  type t_DeepModelTy'0
+  
+  function deep_model'2 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Self_'0) : t_DeepModelTy'0
+  
+  function deep_model'3 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Rhs'0) : t_DeepModelTy'0
+  
+  type t_Ordering'0  =
+    | C_Less'0
+    | C_Equal'0
+    | C_Greater'0
+  
+  function cmp_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 19 4 19 46] (self : t_DeepModelTy'0) (other : t_DeepModelTy'0) : t_Ordering'0
+    
+  
+  function eq_cmp'0 [#"../../../creusot-contracts/src/logic/ord.rs" 96 4 96 32] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom eq_cmp'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord19] (x = y)
+  = (cmp_log'0 x y = C_Equal'0)
+  
+  function antisym2'0 [#"../../../creusot-contracts/src/logic/ord.rs" 91 4 91 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym2'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord17] cmp_log'0 x y = C_Greater'0)
+   -> ([%#sord18] cmp_log'0 y x = C_Less'0)
+  
+  function antisym1'0 [#"../../../creusot-contracts/src/logic/ord.rs" 83 4 83 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym1'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord15] cmp_log'0 x y = C_Less'0)
+   -> ([%#sord16] cmp_log'0 y x = C_Greater'0)
+  
+  function trans'0 [#"../../../creusot-contracts/src/logic/ord.rs" 75 4 75 53] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) (z : t_DeepModelTy'0) (o : t_Ordering'0) : ()
+    
+  
+  axiom trans'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0, z : t_DeepModelTy'0, o : t_Ordering'0 . ([%#sord12] cmp_log'0 x y
+  = o)  -> ([%#sord13] cmp_log'0 y z = o)  -> ([%#sord14] cmp_log'0 x z = o)
+  
+  function refl'0 [#"../../../creusot-contracts/src/logic/ord.rs" 68 4 68 21] (x : t_DeepModelTy'0) : ()
+  
+  axiom refl'0_spec : forall x : t_DeepModelTy'0 . [%#sord11] cmp_log'0 x x = C_Equal'0
+  
+  function gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 57 4 57 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 63 4 63 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_gt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord10] gt_log'0 x y
+  = (cmp_log'0 x y = C_Greater'0)
+  
+  function ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 46 4 46 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 52 4 52 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_ge_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord9] ge_log'0 x y
+  = (cmp_log'0 x y <> C_Less'0)
+  
+  function lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 35 4 35 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 41 4 41 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_lt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord8] lt_log'0 x y
+  = (cmp_log'0 x y = C_Less'0)
+  
+  function le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 24 4 24 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 30 4 30 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_le_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord7] le_log'0 x y
+  = (cmp_log'0 x y <> C_Greater'0)
+  
+  type t_Option'0  =
+    | C_None'0
+    | C_Some'0 (t_Ordering'0)
+  
+  let rec partial_cmp'0 (self:t_Self_'0) (other:t_Rhs'0) (return'  (ret:t_Option'0))= {[@expl:partial_cmp 'self' type invariant] inv'0 self}
+    {[@expl:partial_cmp 'other' type invariant] inv'1 other}
+    any
+    [ return' (result:t_Option'0)-> {[%#scmp5] result = C_Some'0 (cmp_log'0 (deep_model'2 self) (deep_model'3 other))}
+      (! return' {result}) ]
+    
+  
+  let rec v_Some'0 (input:t_Option'0) (ret  (field_0:t_Ordering'0))= any
+    [ good (field_0:t_Ordering'0)-> {C_Some'0 field_0 = input} (! ret {field_0})
+    | bad -> {forall field_0 : t_Ordering'0 [C_Some'0 field_0 : t_Option'0] . C_Some'0 field_0 <> input}
+      (! {false}
+      any) ]
+    
+  
+  use prelude.prelude.Intrinsic
+  
+  function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Self_'0) : t_DeepModelTy'0 =
+    [%#smodel6] deep_model'2 self
+  
+  function deep_model'1 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Rhs'0) : t_DeepModelTy'0 =
+    [%#smodel6] deep_model'3 self
+  
+  meta "compute_max_steps" 1000000
+  
+  let rec extern_spec_std_cmp_PartialOrd_Rhs_gt_body'0 (self_:t_Self_'0) (other:t_Rhs'0) (return'  (ret:bool))= {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_gt_body 'self_' type invariant] [%#scmp2] inv'0 self_}
+    {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_gt_body 'other' type invariant] [%#scmp3] inv'1 other}
+    (! bb0
+    [ bb0 = s0 [ s0 = partial_cmp'0 {self_} {other} (fun (_ret':t_Option'0) ->  [ &_4 <- _ret' ] s1) | s1 = bb1 ] 
+    | bb1 = any [ br0 -> {_4 = C_None'0 } (! bb8) | br1 (x0:t_Ordering'0)-> {_4 = C_Some'0 x0} (! bb3) ] 
+    | bb8 = bb2
+    | bb3 = v_Some'0 {_4}
+        (fun (r0'0:t_Ordering'0) ->
+          any
+          [ br0 -> {r0'0 = C_Less'0 } (! bb2)
+          | br1 -> {r0'0 = C_Equal'0 } (! bb2)
+          | br2 -> {r0'0 = C_Greater'0 } (! bb4) ]
+          )
+    | bb2 = s0 [ s0 =  [ &_0 <- [%#scmp0] false ] s1 | s1 = bb6 ] 
+    | bb4 = bb5
+    | bb5 = s0 [ s0 =  [ &_0 <- [%#scmp1] true ] s1 | s1 = bb6 ] 
+    | bb6 = return' {_0} ]
+    )
+    [ & _0 : bool = any_l () | & self_ : t_Self_'0 = self_ | & other : t_Rhs'0 = other | & _4 : t_Option'0 = any_l () ]
+    
+    [ return' (result:bool)-> {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_gt_body ensures] [%#scmp4] result
+      = gt_log'0 (deep_model'0 self_) (deep_model'1 other)}
+      (! return' {result}) ]
+    
+end
+module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_PartialOrd_Rhs_ge_body [#"../../../creusot-contracts/src/std/cmp.rs" 27 32 60 18]
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 63 29 63 34
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 62 69 62 73
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 60 29 60 34
+  let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 59 26 59 77
+  let%span scmp5 = "../../../creusot-contracts/src/std/cmp.rs" 32 26 32 91
+  let%span smodel6 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
+  let%span sord7 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
+  let%span sord8 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
+  let%span sord9 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
+  let%span sord10 = "../../../creusot-contracts/src/logic/ord.rs" 62 14 62 64
+  let%span sord11 = "../../../creusot-contracts/src/logic/ord.rs" 67 14 67 45
+  let%span sord12 = "../../../creusot-contracts/src/logic/ord.rs" 72 15 72 32
+  let%span sord13 = "../../../creusot-contracts/src/logic/ord.rs" 73 15 73 32
+  let%span sord14 = "../../../creusot-contracts/src/logic/ord.rs" 74 14 74 31
+  let%span sord15 = "../../../creusot-contracts/src/logic/ord.rs" 81 15 81 45
+  let%span sord16 = "../../../creusot-contracts/src/logic/ord.rs" 82 14 82 47
+  let%span sord17 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48
+  let%span sord18 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44
+  let%span sord19 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59
+  let%span sinvariant20 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  
+  use prelude.prelude.Borrow
+  
+  type t_Self_'0
+  
+  predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Self_'0) =
+    [%#sinvariant20] inv'2 self
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_Self_'0 [inv'0 x] . inv'0 x = invariant'0 x
+  
+  type t_Rhs'0
+  
+  predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Rhs'0)
+  
+  predicate invariant'1 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Rhs'0) =
+    [%#sinvariant20] inv'3 self
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Rhs'0)
+  
+  axiom inv_axiom'1 [@rewrite] : forall x : t_Rhs'0 [inv'1 x] . inv'1 x = invariant'1 x
+  
+  type t_DeepModelTy'0
+  
+  function deep_model'2 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Self_'0) : t_DeepModelTy'0
+  
+  function deep_model'3 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Rhs'0) : t_DeepModelTy'0
+  
+  type t_Ordering'0  =
+    | C_Less'0
+    | C_Equal'0
+    | C_Greater'0
+  
+  function cmp_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 19 4 19 46] (self : t_DeepModelTy'0) (other : t_DeepModelTy'0) : t_Ordering'0
+    
+  
+  function eq_cmp'0 [#"../../../creusot-contracts/src/logic/ord.rs" 96 4 96 32] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom eq_cmp'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord19] (x = y)
+  = (cmp_log'0 x y = C_Equal'0)
+  
+  function antisym2'0 [#"../../../creusot-contracts/src/logic/ord.rs" 91 4 91 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym2'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord17] cmp_log'0 x y = C_Greater'0)
+   -> ([%#sord18] cmp_log'0 y x = C_Less'0)
+  
+  function antisym1'0 [#"../../../creusot-contracts/src/logic/ord.rs" 83 4 83 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym1'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord15] cmp_log'0 x y = C_Less'0)
+   -> ([%#sord16] cmp_log'0 y x = C_Greater'0)
+  
+  function trans'0 [#"../../../creusot-contracts/src/logic/ord.rs" 75 4 75 53] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) (z : t_DeepModelTy'0) (o : t_Ordering'0) : ()
+    
+  
+  axiom trans'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0, z : t_DeepModelTy'0, o : t_Ordering'0 . ([%#sord12] cmp_log'0 x y
+  = o)  -> ([%#sord13] cmp_log'0 y z = o)  -> ([%#sord14] cmp_log'0 x z = o)
+  
+  function refl'0 [#"../../../creusot-contracts/src/logic/ord.rs" 68 4 68 21] (x : t_DeepModelTy'0) : ()
+  
+  axiom refl'0_spec : forall x : t_DeepModelTy'0 . [%#sord11] cmp_log'0 x x = C_Equal'0
+  
+  function gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 57 4 57 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 63 4 63 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_gt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord10] gt_log'0 x y
+  = (cmp_log'0 x y = C_Greater'0)
+  
+  function ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 46 4 46 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 52 4 52 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_ge_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord9] ge_log'0 x y
+  = (cmp_log'0 x y <> C_Less'0)
+  
+  function lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 35 4 35 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 41 4 41 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_lt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord8] lt_log'0 x y
+  = (cmp_log'0 x y = C_Less'0)
+  
+  function le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 24 4 24 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 30 4 30 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_le_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord7] le_log'0 x y
+  = (cmp_log'0 x y <> C_Greater'0)
+  
+  type t_Option'0  =
+    | C_None'0
+    | C_Some'0 (t_Ordering'0)
+  
+  let rec partial_cmp'0 (self:t_Self_'0) (other:t_Rhs'0) (return'  (ret:t_Option'0))= {[@expl:partial_cmp 'self' type invariant] inv'0 self}
+    {[@expl:partial_cmp 'other' type invariant] inv'1 other}
+    any
+    [ return' (result:t_Option'0)-> {[%#scmp5] result = C_Some'0 (cmp_log'0 (deep_model'2 self) (deep_model'3 other))}
+      (! return' {result}) ]
+    
+  
+  let rec v_Some'0 (input:t_Option'0) (ret  (field_0:t_Ordering'0))= any
+    [ good (field_0:t_Ordering'0)-> {C_Some'0 field_0 = input} (! ret {field_0})
+    | bad -> {forall field_0 : t_Ordering'0 [C_Some'0 field_0 : t_Option'0] . C_Some'0 field_0 <> input}
+      (! {false}
+      any) ]
+    
+  
+  use prelude.prelude.Intrinsic
+  
+  function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Self_'0) : t_DeepModelTy'0 =
+    [%#smodel6] deep_model'2 self
+  
+  function deep_model'1 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Rhs'0) : t_DeepModelTy'0 =
+    [%#smodel6] deep_model'3 self
+  
+  meta "compute_max_steps" 1000000
+  
+  let rec extern_spec_std_cmp_PartialOrd_Rhs_ge_body'0 (self_:t_Self_'0) (other:t_Rhs'0) (return'  (ret:bool))= {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_ge_body 'self_' type invariant] [%#scmp2] inv'0 self_}
+    {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_ge_body 'other' type invariant] [%#scmp3] inv'1 other}
+    (! bb0
+    [ bb0 = s0 [ s0 = partial_cmp'0 {self_} {other} (fun (_ret':t_Option'0) ->  [ &_4 <- _ret' ] s1) | s1 = bb1 ] 
+    | bb1 = any [ br0 -> {_4 = C_None'0 } (! bb8) | br1 (x0:t_Ordering'0)-> {_4 = C_Some'0 x0} (! bb3) ] 
+    | bb8 = bb2
+    | bb3 = v_Some'0 {_4}
+        (fun (r0'0:t_Ordering'0) ->
+          any
+          [ br0 -> {r0'0 = C_Less'0 } (! bb2)
+          | br1 -> {r0'0 = C_Equal'0 } (! bb4)
+          | br2 -> {r0'0 = C_Greater'0 } (! bb4) ]
+          )
+    | bb2 = s0 [ s0 =  [ &_0 <- [%#scmp0] false ] s1 | s1 = bb6 ] 
+    | bb4 = bb5
+    | bb5 = s0 [ s0 =  [ &_0 <- [%#scmp1] true ] s1 | s1 = bb6 ] 
+    | bb6 = return' {_0} ]
+    )
+    [ & _0 : bool = any_l () | & self_ : t_Self_'0 = self_ | & other : t_Rhs'0 = other | & _4 : t_Option'0 = any_l () ]
+    
+    [ return' (result:bool)-> {[@expl:extern_spec_std_cmp_PartialOrd_Rhs_ge_body ensures] [%#scmp4] result
+      = ge_log'0 (deep_model'0 self_) (deep_model'1 other)}
+      (! return' {result}) ]
+    
+end
+module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_Ord_max_body [#"../../../creusot-contracts/src/std/cmp.rs" 68 18 80 18]
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 80 29 80 30
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 80 41 80 45
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 75 26 75 66
+  let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 76 26 76 63
+  let%span scmp5 = "../../../creusot-contracts/src/std/cmp.rs" 43 26 43 77
+  let%span smodel6 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
+  let%span sord7 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
+  let%span sord8 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
+  let%span sord9 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
+  let%span sord10 = "../../../creusot-contracts/src/logic/ord.rs" 62 14 62 64
+  let%span sord11 = "../../../creusot-contracts/src/logic/ord.rs" 67 14 67 45
+  let%span sord12 = "../../../creusot-contracts/src/logic/ord.rs" 72 15 72 32
+  let%span sord13 = "../../../creusot-contracts/src/logic/ord.rs" 73 15 73 32
+  let%span sord14 = "../../../creusot-contracts/src/logic/ord.rs" 74 14 74 31
+  let%span sord15 = "../../../creusot-contracts/src/logic/ord.rs" 81 15 81 45
+  let%span sord16 = "../../../creusot-contracts/src/logic/ord.rs" 82 14 82 47
+  let%span sord17 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48
+  let%span sord18 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44
+  let%span sord19 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59
+  let%span sinvariant20 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  
+  use prelude.prelude.Borrow
+  
+  type t_Self_'0
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Self_'0) =
+    [%#sinvariant20] inv'0 self
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_Self_'0 [inv'1 x] . inv'1 x = invariant'0 x
+  
+  type t_DeepModelTy'0
+  
+  function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Self_'0) : t_DeepModelTy'0
+  
+  function deep_model'1 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Self_'0) : t_DeepModelTy'0 =
+    [%#smodel6] deep_model'0 self
+  
+  type t_Ordering'0  =
+    | C_Less'0
+    | C_Equal'0
+    | C_Greater'0
+  
+  function cmp_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 19 4 19 46] (self : t_DeepModelTy'0) (other : t_DeepModelTy'0) : t_Ordering'0
+    
+  
+  function eq_cmp'0 [#"../../../creusot-contracts/src/logic/ord.rs" 96 4 96 32] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom eq_cmp'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord19] (x = y)
+  = (cmp_log'0 x y = C_Equal'0)
+  
+  function antisym2'0 [#"../../../creusot-contracts/src/logic/ord.rs" 91 4 91 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym2'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord17] cmp_log'0 x y = C_Greater'0)
+   -> ([%#sord18] cmp_log'0 y x = C_Less'0)
+  
+  function antisym1'0 [#"../../../creusot-contracts/src/logic/ord.rs" 83 4 83 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym1'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord15] cmp_log'0 x y = C_Less'0)
+   -> ([%#sord16] cmp_log'0 y x = C_Greater'0)
+  
+  function trans'0 [#"../../../creusot-contracts/src/logic/ord.rs" 75 4 75 53] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) (z : t_DeepModelTy'0) (o : t_Ordering'0) : ()
+    
+  
+  axiom trans'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0, z : t_DeepModelTy'0, o : t_Ordering'0 . ([%#sord12] cmp_log'0 x y
+  = o)  -> ([%#sord13] cmp_log'0 y z = o)  -> ([%#sord14] cmp_log'0 x z = o)
+  
+  function refl'0 [#"../../../creusot-contracts/src/logic/ord.rs" 68 4 68 21] (x : t_DeepModelTy'0) : ()
+  
+  axiom refl'0_spec : forall x : t_DeepModelTy'0 . [%#sord11] cmp_log'0 x x = C_Equal'0
+  
+  function gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 57 4 57 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 63 4 63 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_gt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord10] gt_log'0 x y
+  = (cmp_log'0 x y = C_Greater'0)
+  
+  function ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 46 4 46 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 52 4 52 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_ge_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord9] ge_log'0 x y
+  = (cmp_log'0 x y <> C_Less'0)
+  
+  function lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 35 4 35 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 41 4 41 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_lt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord8] lt_log'0 x y
+  = (cmp_log'0 x y = C_Less'0)
+  
+  function le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 24 4 24 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 30 4 30 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_le_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord7] le_log'0 x y
+  = (cmp_log'0 x y <> C_Greater'0)
+  
+  let rec le'0 (self:t_Self_'0) (other:t_Self_'0) (return'  (ret:bool))= {[@expl:le 'self' type invariant] inv'1 self}
+    {[@expl:le 'other' type invariant] inv'1 other}
+    any
+    [ return' (result:bool)-> {[%#scmp5] result = le_log'0 (deep_model'1 self) (deep_model'1 other)}
+      (! return' {result}) ]
+    
+  
+  predicate resolve'0 [#"../../../creusot-contracts/src/resolve.rs" 19 0 19 40] (_1 : t_Self_'0)
+  
+  use prelude.prelude.Intrinsic
+  
+  meta "compute_max_steps" 1000000
+  
+  let rec extern_spec_std_cmp_Ord_max_body'0 (self_:t_Self_'0) (o:t_Self_'0) (return'  (ret:t_Self_'0))= {[@expl:extern_spec_std_cmp_Ord_max_body 'self_' type invariant] [%#scmp0] inv'0 self_}
+    {[@expl:extern_spec_std_cmp_Ord_max_body 'o' type invariant] [%#scmp1] inv'0 o}
+    (! bb0
+    [ bb0 = bb1
+    | bb1 = bb2
+    | bb2 = bb3
+    | bb3 = bb4
+    | bb4 = bb5
+    | bb5 = s0 [ s0 = le'0 {self_} {o} (fun (_ret':bool) ->  [ &_8 <- _ret' ] s1) | s1 = bb6 ] 
+    | bb6 = any [ br0 -> {_8 = false} (! bb8) | br1 -> {_8} (! bb7) ] 
+    | bb7 = s0
+      [ s0 = {[@expl:type invariant] inv'0 self_} s1 | s1 = -{resolve'0 self_}- s2 | s2 =  [ &_0 <- o ] s3 | s3 = bb9 ]
+      
+    | bb8 = s0
+      [ s0 = {[@expl:type invariant] inv'0 o} s1 | s1 = -{resolve'0 o}- s2 | s2 =  [ &_0 <- self_ ] s3 | s3 = bb9 ]
+      
+    | bb9 = bb10
+    | bb10 = bb11
+    | bb11 = return' {_0} ]
+    ) [ & _0 : t_Self_'0 = any_l () | & self_ : t_Self_'0 = self_ | & o : t_Self_'0 = o | & _8 : bool = any_l () ] 
+    [ return' (result:t_Self_'0)-> {[@expl:extern_spec_std_cmp_Ord_max_body result type invariant] [%#scmp2] inv'0 result}
+      {[@expl:extern_spec_std_cmp_Ord_max_body ensures #0] [%#scmp3] ge_log'0 (deep_model'0 result) (deep_model'0 self_)}
+      {[@expl:extern_spec_std_cmp_Ord_max_body ensures #1] [%#scmp4] ge_log'0 (deep_model'0 result) (deep_model'0 o)}
+      {[@expl:extern_spec_std_cmp_Ord_max_body ensures #2] [%#scmp0] result = self_ \/ result = o}
+      {[@expl:extern_spec_std_cmp_Ord_max_body ensures #3] [%#scmp0] le_log'0 (deep_model'0 self_) (deep_model'0 o)
+       -> result = o}
+      {[@expl:extern_spec_std_cmp_Ord_max_body ensures #4] [%#scmp0] lt_log'0 (deep_model'0 o) (deep_model'0 self_)
+       -> result = self_}
+      (! return' {result}) ]
+    
+end
+module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_Ord_min_body [#"../../../creusot-contracts/src/std/cmp.rs" 68 18 89 18]
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 89 29 89 30
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 89 41 89 45
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 84 26 84 66
+  let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 85 26 85 63
+  let%span scmp5 = "../../../creusot-contracts/src/std/cmp.rs" 88 26 88 77
+  let%span scmp6 = "../../../creusot-contracts/src/std/cmp.rs" 35 26 35 76
+  let%span smodel7 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
+  let%span sord8 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
+  let%span sord9 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
+  let%span sord10 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
+  let%span sord11 = "../../../creusot-contracts/src/logic/ord.rs" 62 14 62 64
+  let%span sord12 = "../../../creusot-contracts/src/logic/ord.rs" 67 14 67 45
+  let%span sord13 = "../../../creusot-contracts/src/logic/ord.rs" 72 15 72 32
+  let%span sord14 = "../../../creusot-contracts/src/logic/ord.rs" 73 15 73 32
+  let%span sord15 = "../../../creusot-contracts/src/logic/ord.rs" 74 14 74 31
+  let%span sord16 = "../../../creusot-contracts/src/logic/ord.rs" 81 15 81 45
+  let%span sord17 = "../../../creusot-contracts/src/logic/ord.rs" 82 14 82 47
+  let%span sord18 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48
+  let%span sord19 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44
+  let%span sord20 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59
+  let%span sinvariant21 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  
+  use prelude.prelude.Borrow
+  
+  type t_Self_'0
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Self_'0) =
+    [%#sinvariant21] inv'0 self
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_Self_'0 [inv'1 x] . inv'1 x = invariant'0 x
+  
+  type t_DeepModelTy'0
+  
+  function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Self_'0) : t_DeepModelTy'0
+  
+  function deep_model'1 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Self_'0) : t_DeepModelTy'0 =
+    [%#smodel7] deep_model'0 self
+  
+  type t_Ordering'0  =
+    | C_Less'0
+    | C_Equal'0
+    | C_Greater'0
+  
+  function cmp_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 19 4 19 46] (self : t_DeepModelTy'0) (other : t_DeepModelTy'0) : t_Ordering'0
+    
+  
+  function eq_cmp'0 [#"../../../creusot-contracts/src/logic/ord.rs" 96 4 96 32] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom eq_cmp'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord20] (x = y)
+  = (cmp_log'0 x y = C_Equal'0)
+  
+  function antisym2'0 [#"../../../creusot-contracts/src/logic/ord.rs" 91 4 91 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym2'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord18] cmp_log'0 x y = C_Greater'0)
+   -> ([%#sord19] cmp_log'0 y x = C_Less'0)
+  
+  function antisym1'0 [#"../../../creusot-contracts/src/logic/ord.rs" 83 4 83 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym1'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord16] cmp_log'0 x y = C_Less'0)
+   -> ([%#sord17] cmp_log'0 y x = C_Greater'0)
+  
+  function trans'0 [#"../../../creusot-contracts/src/logic/ord.rs" 75 4 75 53] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) (z : t_DeepModelTy'0) (o : t_Ordering'0) : ()
+    
+  
+  axiom trans'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0, z : t_DeepModelTy'0, o : t_Ordering'0 . ([%#sord13] cmp_log'0 x y
+  = o)  -> ([%#sord14] cmp_log'0 y z = o)  -> ([%#sord15] cmp_log'0 x z = o)
+  
+  function refl'0 [#"../../../creusot-contracts/src/logic/ord.rs" 68 4 68 21] (x : t_DeepModelTy'0) : ()
+  
+  axiom refl'0_spec : forall x : t_DeepModelTy'0 . [%#sord12] cmp_log'0 x x = C_Equal'0
+  
+  function gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 57 4 57 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 63 4 63 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_gt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord11] gt_log'0 x y
+  = (cmp_log'0 x y = C_Greater'0)
+  
+  function ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 46 4 46 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 52 4 52 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_ge_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord10] ge_log'0 x y
+  = (cmp_log'0 x y <> C_Less'0)
+  
+  function lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 35 4 35 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 41 4 41 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_lt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord9] lt_log'0 x y
+  = (cmp_log'0 x y = C_Less'0)
+  
+  function le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 24 4 24 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 30 4 30 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_le_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord8] le_log'0 x y
+  = (cmp_log'0 x y <> C_Greater'0)
+  
+  let rec lt'0 (self:t_Self_'0) (other:t_Self_'0) (return'  (ret:bool))= {[@expl:lt 'self' type invariant] inv'1 self}
+    {[@expl:lt 'other' type invariant] inv'1 other}
+    any
+    [ return' (result:bool)-> {[%#scmp6] result = lt_log'0 (deep_model'1 self) (deep_model'1 other)}
+      (! return' {result}) ]
+    
+  
+  predicate resolve'0 [#"../../../creusot-contracts/src/resolve.rs" 19 0 19 40] (_1 : t_Self_'0)
+  
+  use prelude.prelude.Intrinsic
+  
+  meta "compute_max_steps" 1000000
+  
+  let rec extern_spec_std_cmp_Ord_min_body'0 (self_:t_Self_'0) (o:t_Self_'0) (return'  (ret:t_Self_'0))= {[@expl:extern_spec_std_cmp_Ord_min_body 'self_' type invariant] [%#scmp0] inv'0 self_}
+    {[@expl:extern_spec_std_cmp_Ord_min_body 'o' type invariant] [%#scmp1] inv'0 o}
+    (! bb0
+    [ bb0 = bb1
+    | bb1 = bb2
+    | bb2 = bb3
+    | bb3 = bb4
+    | bb4 = bb5
+    | bb5 = s0 [ s0 = lt'0 {self_} {o} (fun (_ret':bool) ->  [ &_8 <- _ret' ] s1) | s1 = bb6 ] 
+    | bb6 = any [ br0 -> {_8 = false} (! bb8) | br1 -> {_8} (! bb7) ] 
+    | bb7 = s0
+      [ s0 = {[@expl:type invariant] inv'0 o} s1 | s1 = -{resolve'0 o}- s2 | s2 =  [ &_0 <- self_ ] s3 | s3 = bb9 ]
+      
+    | bb8 = s0
+      [ s0 = {[@expl:type invariant] inv'0 self_} s1 | s1 = -{resolve'0 self_}- s2 | s2 =  [ &_0 <- o ] s3 | s3 = bb9 ]
+      
+    | bb9 = bb10
+    | bb10 = bb11
+    | bb11 = return' {_0} ]
+    ) [ & _0 : t_Self_'0 = any_l () | & self_ : t_Self_'0 = self_ | & o : t_Self_'0 = o | & _8 : bool = any_l () ] 
+    [ return' (result:t_Self_'0)-> {[@expl:extern_spec_std_cmp_Ord_min_body result type invariant] [%#scmp2] inv'0 result}
+      {[@expl:extern_spec_std_cmp_Ord_min_body ensures #0] [%#scmp3] le_log'0 (deep_model'0 result) (deep_model'0 self_)}
+      {[@expl:extern_spec_std_cmp_Ord_min_body ensures #1] [%#scmp4] le_log'0 (deep_model'0 result) (deep_model'0 o)}
+      {[@expl:extern_spec_std_cmp_Ord_min_body ensures #2] [%#scmp0] result = self_ \/ result = o}
+      {[@expl:extern_spec_std_cmp_Ord_min_body ensures #3] [%#scmp0] lt_log'0 (deep_model'0 self_) (deep_model'0 o)
+       -> result = self_}
+      {[@expl:extern_spec_std_cmp_Ord_min_body ensures #4] [%#scmp5] le_log'0 (deep_model'0 o) (deep_model'0 self_)
+       -> result = o}
+      (! return' {result}) ]
+    
+end
+module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_Ord_clamp_body [#"../../../creusot-contracts/src/std/cmp.rs" 68 18 102 18]
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 102 31 102 34
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 102 42 102 45
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 93 27 93 63
+  let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 102 56 102 60
+  let%span scmp5 = "../../../creusot-contracts/src/std/cmp.rs" 94 26 94 65
+  let%span scmp6 = "../../../creusot-contracts/src/std/cmp.rs" 95 26 95 65
+  let%span scmp7 = "../../../creusot-contracts/src/std/cmp.rs" 97 16 101 43
+  let%span scmp8 = "../../../creusot-contracts/src/std/cmp.rs" 51 26 51 76
+  let%span scmp9 = "../../../creusot-contracts/src/std/cmp.rs" 35 26 35 76
+  let%span smodel10 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
+  let%span sord11 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
+  let%span sord12 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
+  let%span sord13 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
+  let%span sord14 = "../../../creusot-contracts/src/logic/ord.rs" 62 14 62 64
+  let%span sord15 = "../../../creusot-contracts/src/logic/ord.rs" 67 14 67 45
+  let%span sord16 = "../../../creusot-contracts/src/logic/ord.rs" 72 15 72 32
+  let%span sord17 = "../../../creusot-contracts/src/logic/ord.rs" 73 15 73 32
+  let%span sord18 = "../../../creusot-contracts/src/logic/ord.rs" 74 14 74 31
+  let%span sord19 = "../../../creusot-contracts/src/logic/ord.rs" 81 15 81 45
+  let%span sord20 = "../../../creusot-contracts/src/logic/ord.rs" 82 14 82 47
+  let%span sord21 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48
+  let%span sord22 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44
+  let%span sord23 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59
+  let%span sinvariant24 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  
+  use prelude.prelude.Borrow
+  
+  type t_Self_'0
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Self_'0) =
+    [%#sinvariant24] inv'0 self
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Self_'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_Self_'0 [inv'1 x] . inv'1 x = invariant'0 x
+  
+  type t_DeepModelTy'0
+  
+  function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_Self_'0) : t_DeepModelTy'0
+  
+  function deep_model'1 [#"../../../creusot-contracts/src/model.rs" 82 4 82 44] (self : t_Self_'0) : t_DeepModelTy'0 =
+    [%#smodel10] deep_model'0 self
+  
+  type t_Ordering'0  =
+    | C_Less'0
+    | C_Equal'0
+    | C_Greater'0
+  
+  function cmp_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 19 4 19 46] (self : t_DeepModelTy'0) (other : t_DeepModelTy'0) : t_Ordering'0
+    
+  
+  function eq_cmp'0 [#"../../../creusot-contracts/src/logic/ord.rs" 96 4 96 32] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom eq_cmp'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord23] (x = y)
+  = (cmp_log'0 x y = C_Equal'0)
+  
+  function antisym2'0 [#"../../../creusot-contracts/src/logic/ord.rs" 91 4 91 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym2'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord21] cmp_log'0 x y = C_Greater'0)
+   -> ([%#sord22] cmp_log'0 y x = C_Less'0)
+  
+  function antisym1'0 [#"../../../creusot-contracts/src/logic/ord.rs" 83 4 83 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym1'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord19] cmp_log'0 x y = C_Less'0)
+   -> ([%#sord20] cmp_log'0 y x = C_Greater'0)
+  
+  function trans'0 [#"../../../creusot-contracts/src/logic/ord.rs" 75 4 75 53] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) (z : t_DeepModelTy'0) (o : t_Ordering'0) : ()
+    
+  
+  axiom trans'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0, z : t_DeepModelTy'0, o : t_Ordering'0 . ([%#sord16] cmp_log'0 x y
+  = o)  -> ([%#sord17] cmp_log'0 y z = o)  -> ([%#sord18] cmp_log'0 x z = o)
+  
+  function refl'0 [#"../../../creusot-contracts/src/logic/ord.rs" 68 4 68 21] (x : t_DeepModelTy'0) : ()
+  
+  axiom refl'0_spec : forall x : t_DeepModelTy'0 . [%#sord15] cmp_log'0 x x = C_Equal'0
+  
+  function gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 57 4 57 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 63 4 63 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_gt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord14] gt_log'0 x y
+  = (cmp_log'0 x y = C_Greater'0)
+  
+  function ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 46 4 46 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 52 4 52 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_ge_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord13] ge_log'0 x y
+  = (cmp_log'0 x y <> C_Less'0)
+  
+  function lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 35 4 35 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 41 4 41 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_lt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord12] lt_log'0 x y
+  = (cmp_log'0 x y = C_Less'0)
+  
+  function le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 24 4 24 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 30 4 30 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_le_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord11] le_log'0 x y
+  = (cmp_log'0 x y <> C_Greater'0)
+  
+  let rec gt'0 (self:t_Self_'0) (other:t_Self_'0) (return'  (ret:bool))= {[@expl:gt 'self' type invariant] inv'1 self}
+    {[@expl:gt 'other' type invariant] inv'1 other}
+    any
+    [ return' (result:bool)-> {[%#scmp8] result = gt_log'0 (deep_model'1 self) (deep_model'1 other)}
+      (! return' {result}) ]
+    
+  
+  predicate resolve'0 [#"../../../creusot-contracts/src/resolve.rs" 19 0 19 40] (_1 : t_Self_'0)
+  
+  let rec lt'0 (self:t_Self_'0) (other:t_Self_'0) (return'  (ret:bool))= {[@expl:lt 'self' type invariant] inv'1 self}
+    {[@expl:lt 'other' type invariant] inv'1 other}
+    any
+    [ return' (result:bool)-> {[%#scmp9] result = lt_log'0 (deep_model'1 self) (deep_model'1 other)}
+      (! return' {result}) ]
+    
+  
+  use prelude.prelude.Intrinsic
+  
+  meta "compute_max_steps" 1000000
+  
+  let rec extern_spec_std_cmp_Ord_clamp_body'0 (self_:t_Self_'0) (min:t_Self_'0) (max:t_Self_'0) (return'  (ret:t_Self_'0))= {[@expl:extern_spec_std_cmp_Ord_clamp_body 'self_' type invariant] [%#scmp0] inv'0 self_}
+    {[@expl:extern_spec_std_cmp_Ord_clamp_body 'min' type invariant] [%#scmp1] inv'0 min}
+    {[@expl:extern_spec_std_cmp_Ord_clamp_body 'max' type invariant] [%#scmp2] inv'0 max}
+    {[@expl:extern_spec_std_cmp_Ord_clamp_body requires] [%#scmp3] le_log'0 (deep_model'0 min) (deep_model'0 max)}
+    (! bb0
+    [ bb0 = bb1
+    | bb1 = bb2
+    | bb2 = bb3
+    | bb3 = bb4
+    | bb4 = bb5
+    | bb5 = s0 [ s0 = gt'0 {self_} {max} (fun (_ret':bool) ->  [ &_9 <- _ret' ] s1) | s1 = bb6 ] 
+    | bb6 = any [ br0 -> {_9 = false} (! bb8) | br1 -> {_9} (! bb7) ] 
+    | bb7 = s0
+      [ s0 = {[@expl:type invariant] inv'0 min} s1
+      | s1 = -{resolve'0 min}- s2
+      | s2 = {[@expl:type invariant] inv'0 self_} s3
+      | s3 = -{resolve'0 self_}- s4
+      | s4 =  [ &_0 <- max ] s5
+      | s5 = bb13 ]
+      
+    | bb8 = s0
+      [ s0 = {[@expl:type invariant] inv'0 max} s1
+      | s1 = -{resolve'0 max}- s2
+      | s2 = lt'0 {self_} {min} (fun (_ret':bool) ->  [ &_12 <- _ret' ] s3)
+      | s3 = bb9 ]
+      
+    | bb9 = any [ br0 -> {_12 = false} (! bb11) | br1 -> {_12} (! bb10) ] 
+    | bb10 = s0
+      [ s0 = {[@expl:type invariant] inv'0 self_} s1
+      | s1 = -{resolve'0 self_}- s2
+      | s2 =  [ &_0 <- min ] s3
+      | s3 = bb12 ]
+      
+    | bb11 = s0
+      [ s0 = {[@expl:type invariant] inv'0 min} s1 | s1 = -{resolve'0 min}- s2 | s2 =  [ &_0 <- self_ ] s3 | s3 = bb12 ]
+      
+    | bb12 = bb13
+    | bb13 = bb14
+    | bb14 = bb15
+    | bb15 = bb16
+    | bb16 = return' {_0} ]
+    )
+    [ & _0 : t_Self_'0 = any_l ()
+    | & self_ : t_Self_'0 = self_
+    | & min : t_Self_'0 = min
+    | & max : t_Self_'0 = max
+    | & _9 : bool = any_l ()
+    | & _12 : bool = any_l () ]
+    
+    [ return' (result:t_Self_'0)-> {[@expl:extern_spec_std_cmp_Ord_clamp_body result type invariant] [%#scmp4] inv'0 result}
+      {[@expl:extern_spec_std_cmp_Ord_clamp_body ensures #0] [%#scmp5] ge_log'0 (deep_model'0 result) (deep_model'0 min)}
+      {[@expl:extern_spec_std_cmp_Ord_clamp_body ensures #1] [%#scmp6] le_log'0 (deep_model'0 result) (deep_model'0 max)}
+      {[@expl:extern_spec_std_cmp_Ord_clamp_body ensures #2] [%#scmp0] result = self_ \/ result = min \/ result = max}
+      {[@expl:extern_spec_std_cmp_Ord_clamp_body ensures #3] [%#scmp7] if gt_log'0 (deep_model'0 self_) (deep_model'0 max) then
+        result = max
+      else
+        if lt_log'0 (deep_model'0 self_) (deep_model'0 min) then result = min else result = self_
+      }
+      (! return' {result}) ]
+    
+end
+module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_max_body [#"../../../creusot-contracts/src/std/cmp.rs" 112 12 113 66]
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 112 22 112 24
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 112 29 112 31
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 112 39 112 40
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 107 22 107 60
+  let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 108 22 108 60
+  let%span scmp5 = "../../../creusot-contracts/src/std/cmp.rs" 109 22 109 50
+  let%span scmp6 = "../../../creusot-contracts/src/std/cmp.rs" 110 22 110 73
+  let%span scmp7 = "../../../creusot-contracts/src/std/cmp.rs" 111 22 111 72
+  let%span scmp8 = "../../../creusot-contracts/src/std/cmp.rs" 75 26 75 66
+  let%span scmp9 = "../../../creusot-contracts/src/std/cmp.rs" 76 26 76 63
+  let%span scmp10 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
+  let%span sord11 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
+  let%span sord12 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
+  let%span sord13 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
+  let%span sord14 = "../../../creusot-contracts/src/logic/ord.rs" 62 14 62 64
+  let%span sord15 = "../../../creusot-contracts/src/logic/ord.rs" 67 14 67 45
+  let%span sord16 = "../../../creusot-contracts/src/logic/ord.rs" 72 15 72 32
+  let%span sord17 = "../../../creusot-contracts/src/logic/ord.rs" 73 15 73 32
+  let%span sord18 = "../../../creusot-contracts/src/logic/ord.rs" 74 14 74 31
+  let%span sord19 = "../../../creusot-contracts/src/logic/ord.rs" 81 15 81 45
+  let%span sord20 = "../../../creusot-contracts/src/logic/ord.rs" 82 14 82 47
+  let%span sord21 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48
+  let%span sord22 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44
+  let%span sord23 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59
+  
+  type t_T'0
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0)
+  
+  type t_DeepModelTy'0
+  
+  function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_T'0) : t_DeepModelTy'0
+  
+  type t_Ordering'0  =
+    | C_Less'0
+    | C_Equal'0
+    | C_Greater'0
+  
+  function cmp_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 19 4 19 46] (self : t_DeepModelTy'0) (other : t_DeepModelTy'0) : t_Ordering'0
+    
+  
+  function eq_cmp'0 [#"../../../creusot-contracts/src/logic/ord.rs" 96 4 96 32] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom eq_cmp'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord23] (x = y)
+  = (cmp_log'0 x y = C_Equal'0)
+  
+  function antisym2'0 [#"../../../creusot-contracts/src/logic/ord.rs" 91 4 91 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym2'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord21] cmp_log'0 x y = C_Greater'0)
+   -> ([%#sord22] cmp_log'0 y x = C_Less'0)
+  
+  function antisym1'0 [#"../../../creusot-contracts/src/logic/ord.rs" 83 4 83 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym1'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord19] cmp_log'0 x y = C_Less'0)
+   -> ([%#sord20] cmp_log'0 y x = C_Greater'0)
+  
+  function trans'0 [#"../../../creusot-contracts/src/logic/ord.rs" 75 4 75 53] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) (z : t_DeepModelTy'0) (o : t_Ordering'0) : ()
+    
+  
+  axiom trans'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0, z : t_DeepModelTy'0, o : t_Ordering'0 . ([%#sord16] cmp_log'0 x y
+  = o)  -> ([%#sord17] cmp_log'0 y z = o)  -> ([%#sord18] cmp_log'0 x z = o)
+  
+  function refl'0 [#"../../../creusot-contracts/src/logic/ord.rs" 68 4 68 21] (x : t_DeepModelTy'0) : ()
+  
+  axiom refl'0_spec : forall x : t_DeepModelTy'0 . [%#sord15] cmp_log'0 x x = C_Equal'0
+  
+  function gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 57 4 57 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 63 4 63 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_gt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord14] gt_log'0 x y
+  = (cmp_log'0 x y = C_Greater'0)
+  
+  function ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 46 4 46 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 52 4 52 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_ge_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord13] ge_log'0 x y
+  = (cmp_log'0 x y <> C_Less'0)
+  
+  function lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 35 4 35 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 41 4 41 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_lt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord12] lt_log'0 x y
+  = (cmp_log'0 x y = C_Less'0)
+  
+  function le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 24 4 24 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 30 4 30 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_le_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord11] le_log'0 x y
+  = (cmp_log'0 x y <> C_Greater'0)
+  
+  let rec max'0 (self:t_T'0) (other:t_T'0) (return'  (ret:t_T'0))= {[@expl:max 'self' type invariant] inv'0 self}
+    {[@expl:max 'other' type invariant] inv'0 other}
+    any
+    [ return' (result:t_T'0)-> {inv'0 result}
+      {[%#scmp8] ge_log'0 (deep_model'0 result) (deep_model'0 self)}
+      {[%#scmp9] ge_log'0 (deep_model'0 result) (deep_model'0 other)}
+      {[%#scmp10] result = self \/ result = other}
+      {[%#scmp10] le_log'0 (deep_model'0 self) (deep_model'0 other)  -> result = other}
+      {[%#scmp10] lt_log'0 (deep_model'0 other) (deep_model'0 self)  -> result = self}
+      (! return' {result}) ]
+    
+  
+  use prelude.prelude.Intrinsic
+  
+  meta "compute_max_steps" 1000000
+  
+  let rec extern_spec_std_cmp_max_body'0 (v1:t_T'0) (v2:t_T'0) (return'  (ret:t_T'0))= {[@expl:extern_spec_std_cmp_max_body 'v1' type invariant] [%#scmp0] inv'0 v1}
+    {[@expl:extern_spec_std_cmp_max_body 'v2' type invariant] [%#scmp1] inv'0 v2}
+    (! bb0
+    [ bb0 = bb1
+    | bb1 = bb2
+    | bb2 = bb3
+    | bb3 = bb4
+    | bb4 = bb5
+    | bb5 = s0 [ s0 = max'0 {v1} {v2} (fun (_ret':t_T'0) ->  [ &_0 <- _ret' ] s1) | s1 = bb6 ] 
+    | bb6 = bb7
+    | bb7 = bb8
+    | bb8 = return' {_0} ]
+    ) [ & _0 : t_T'0 = any_l () | & v1 : t_T'0 = v1 | & v2 : t_T'0 = v2 ] 
+    [ return' (result:t_T'0)-> {[@expl:extern_spec_std_cmp_max_body result type invariant] [%#scmp2] inv'0 result}
+      {[@expl:extern_spec_std_cmp_max_body ensures #0] [%#scmp3] ge_log'0 (deep_model'0 result) (deep_model'0 v1)}
+      {[@expl:extern_spec_std_cmp_max_body ensures #1] [%#scmp4] ge_log'0 (deep_model'0 result) (deep_model'0 v2)}
+      {[@expl:extern_spec_std_cmp_max_body ensures #2] [%#scmp5] result = v1 \/ result = v2}
+      {[@expl:extern_spec_std_cmp_max_body ensures #3] [%#scmp6] le_log'0 (deep_model'0 v1) (deep_model'0 v2)
+       -> result = v2}
+      {[@expl:extern_spec_std_cmp_max_body ensures #4] [%#scmp7] lt_log'0 (deep_model'0 v2) (deep_model'0 v1)
+       -> result = v1}
+      (! return' {result}) ]
+    
+end
+module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_min_body [#"../../../creusot-contracts/src/std/cmp.rs" 123 12 124 66]
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 123 22 123 24
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 123 29 123 31
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 123 39 123 40
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 118 22 118 60
+  let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 119 22 119 60
+  let%span scmp5 = "../../../creusot-contracts/src/std/cmp.rs" 120 22 120 50
+  let%span scmp6 = "../../../creusot-contracts/src/std/cmp.rs" 121 22 121 72
+  let%span scmp7 = "../../../creusot-contracts/src/std/cmp.rs" 122 22 122 73
+  let%span scmp8 = "../../../creusot-contracts/src/std/cmp.rs" 84 26 84 66
+  let%span scmp9 = "../../../creusot-contracts/src/std/cmp.rs" 85 26 85 63
+  let%span scmp10 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
+  let%span scmp11 = "../../../creusot-contracts/src/std/cmp.rs" 88 26 88 77
+  let%span sord12 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
+  let%span sord13 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
+  let%span sord14 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
+  let%span sord15 = "../../../creusot-contracts/src/logic/ord.rs" 62 14 62 64
+  let%span sord16 = "../../../creusot-contracts/src/logic/ord.rs" 67 14 67 45
+  let%span sord17 = "../../../creusot-contracts/src/logic/ord.rs" 72 15 72 32
+  let%span sord18 = "../../../creusot-contracts/src/logic/ord.rs" 73 15 73 32
+  let%span sord19 = "../../../creusot-contracts/src/logic/ord.rs" 74 14 74 31
+  let%span sord20 = "../../../creusot-contracts/src/logic/ord.rs" 81 15 81 45
+  let%span sord21 = "../../../creusot-contracts/src/logic/ord.rs" 82 14 82 47
+  let%span sord22 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48
+  let%span sord23 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44
+  let%span sord24 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59
+  
+  type t_T'0
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0)
+  
+  type t_DeepModelTy'0
+  
+  function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_T'0) : t_DeepModelTy'0
+  
+  type t_Ordering'0  =
+    | C_Less'0
+    | C_Equal'0
+    | C_Greater'0
+  
+  function cmp_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 19 4 19 46] (self : t_DeepModelTy'0) (other : t_DeepModelTy'0) : t_Ordering'0
+    
+  
+  function eq_cmp'0 [#"../../../creusot-contracts/src/logic/ord.rs" 96 4 96 32] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom eq_cmp'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord24] (x = y)
+  = (cmp_log'0 x y = C_Equal'0)
+  
+  function antisym2'0 [#"../../../creusot-contracts/src/logic/ord.rs" 91 4 91 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym2'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord22] cmp_log'0 x y = C_Greater'0)
+   -> ([%#sord23] cmp_log'0 y x = C_Less'0)
+  
+  function antisym1'0 [#"../../../creusot-contracts/src/logic/ord.rs" 83 4 83 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom antisym1'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord20] cmp_log'0 x y = C_Less'0)
+   -> ([%#sord21] cmp_log'0 y x = C_Greater'0)
+  
+  function trans'0 [#"../../../creusot-contracts/src/logic/ord.rs" 75 4 75 53] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) (z : t_DeepModelTy'0) (o : t_Ordering'0) : ()
+    
+  
+  axiom trans'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0, z : t_DeepModelTy'0, o : t_Ordering'0 . ([%#sord17] cmp_log'0 x y
+  = o)  -> ([%#sord18] cmp_log'0 y z = o)  -> ([%#sord19] cmp_log'0 x z = o)
+  
+  function refl'0 [#"../../../creusot-contracts/src/logic/ord.rs" 68 4 68 21] (x : t_DeepModelTy'0) : ()
+  
+  axiom refl'0_spec : forall x : t_DeepModelTy'0 . [%#sord16] cmp_log'0 x x = C_Equal'0
+  
+  function gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 57 4 57 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 63 4 63 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_gt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord15] gt_log'0 x y
+  = (cmp_log'0 x y = C_Greater'0)
+  
+  function ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 46 4 46 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 52 4 52 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_ge_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord14] ge_log'0 x y
+  = (cmp_log'0 x y <> C_Less'0)
+  
+  function lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 35 4 35 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 41 4 41 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_lt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord13] lt_log'0 x y
+  = (cmp_log'0 x y = C_Less'0)
+  
+  function le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 24 4 24 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool
+    
+  
+  function cmp_le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 30 4 30 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : ()
+    
+  
+  axiom cmp_le_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord12] le_log'0 x y
+  = (cmp_log'0 x y <> C_Greater'0)
+  
+  let rec min'0 (self:t_T'0) (other:t_T'0) (return'  (ret:t_T'0))= {[@expl:min 'self' type invariant] inv'0 self}
+    {[@expl:min 'other' type invariant] inv'0 other}
+    any
+    [ return' (result:t_T'0)-> {inv'0 result}
+      {[%#scmp8] le_log'0 (deep_model'0 result) (deep_model'0 self)}
+      {[%#scmp9] le_log'0 (deep_model'0 result) (deep_model'0 other)}
+      {[%#scmp10] result = self \/ result = other}
+      {[%#scmp10] lt_log'0 (deep_model'0 self) (deep_model'0 other)  -> result = self}
+      {[%#scmp11] le_log'0 (deep_model'0 other) (deep_model'0 self)  -> result = other}
+      (! return' {result}) ]
+    
+  
+  use prelude.prelude.Intrinsic
+  
+  meta "compute_max_steps" 1000000
+  
+  let rec extern_spec_std_cmp_min_body'0 (v1:t_T'0) (v2:t_T'0) (return'  (ret:t_T'0))= {[@expl:extern_spec_std_cmp_min_body 'v1' type invariant] [%#scmp0] inv'0 v1}
+    {[@expl:extern_spec_std_cmp_min_body 'v2' type invariant] [%#scmp1] inv'0 v2}
+    (! bb0
+    [ bb0 = bb1
+    | bb1 = bb2
+    | bb2 = bb3
+    | bb3 = bb4
+    | bb4 = bb5
+    | bb5 = s0 [ s0 = min'0 {v1} {v2} (fun (_ret':t_T'0) ->  [ &_0 <- _ret' ] s1) | s1 = bb6 ] 
+    | bb6 = bb7
+    | bb7 = bb8
+    | bb8 = return' {_0} ]
+    ) [ & _0 : t_T'0 = any_l () | & v1 : t_T'0 = v1 | & v2 : t_T'0 = v2 ] 
+    [ return' (result:t_T'0)-> {[@expl:extern_spec_std_cmp_min_body result type invariant] [%#scmp2] inv'0 result}
+      {[@expl:extern_spec_std_cmp_min_body ensures #0] [%#scmp3] le_log'0 (deep_model'0 result) (deep_model'0 v1)}
+      {[@expl:extern_spec_std_cmp_min_body ensures #1] [%#scmp4] le_log'0 (deep_model'0 result) (deep_model'0 v2)}
+      {[@expl:extern_spec_std_cmp_min_body ensures #2] [%#scmp5] result = v1 \/ result = v2}
+      {[@expl:extern_spec_std_cmp_min_body ensures #3] [%#scmp6] lt_log'0 (deep_model'0 v1) (deep_model'0 v2)
+       -> result = v1}
+      {[@expl:extern_spec_std_cmp_min_body ensures #4] [%#scmp7] le_log'0 (deep_model'0 v2) (deep_model'0 v1)
+       -> result = v2}
+      (! return' {result}) ]
+    
+end
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log [#"../../../creusot-contracts/src/std/cmp.rs" 156 4 156 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 155 14 155 64
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 153 4 153 10
   let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 25 20 25 56
-  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -172,7 +1779,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log
   
   axiom cmp_le_log'1_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'1 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -190,16 +1797,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log
   
   constant y  : t_Reverse'0
   
-  function cmp_le_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 88 4 88 35] (x : t_Reverse'0) (y : t_Reverse'0) : ()
+  function cmp_le_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 156 4 156 35] (x : t_Reverse'0) (y : t_Reverse'0) : ()
     
   
   goal vc_cmp_le_log'0 : [%#scmp0] le_log'0 x y = (cmp_log'0 x y <> C_Greater'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log [#"../../../creusot-contracts/src/std/cmp.rs" 93 4 93 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 92 14 92 61
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 90 4 90 10
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log [#"../../../creusot-contracts/src/std/cmp.rs" 161 4 161 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 160 14 160 61
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 158 4 158 10
   let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 36 20 36 53
-  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -275,7 +1882,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -293,16 +1900,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log
   
   constant y  : t_Reverse'0
   
-  function cmp_lt_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 93 4 93 35] (x : t_Reverse'0) (y : t_Reverse'0) : ()
+  function cmp_lt_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 161 4 161 35] (x : t_Reverse'0) (y : t_Reverse'0) : ()
     
   
   goal vc_cmp_lt_log'0 : [%#scmp0] lt_log'0 x y = (cmp_log'0 x y = C_Less'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log [#"../../../creusot-contracts/src/std/cmp.rs" 98 4 98 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 97 14 97 61
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 95 4 95 10
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log [#"../../../creusot-contracts/src/std/cmp.rs" 166 4 166 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 165 14 165 61
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 163 4 163 10
   let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 47 20 47 53
-  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -378,7 +1985,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -396,16 +2003,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log
   
   constant y  : t_Reverse'0
   
-  function cmp_ge_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 98 4 98 35] (x : t_Reverse'0) (y : t_Reverse'0) : ()
+  function cmp_ge_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 166 4 166 35] (x : t_Reverse'0) (y : t_Reverse'0) : ()
     
   
   goal vc_cmp_ge_log'0 : [%#scmp0] ge_log'0 x y = (cmp_log'0 x y <> C_Less'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log [#"../../../creusot-contracts/src/std/cmp.rs" 103 4 103 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 102 14 102 64
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 100 4 100 10
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log [#"../../../creusot-contracts/src/std/cmp.rs" 171 4 171 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 170 14 170 64
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 168 4 168 10
   let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 58 20 58 56
-  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -481,7 +2088,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -499,15 +2106,15 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log
   
   constant y  : t_Reverse'0
   
-  function cmp_gt_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 103 4 103 35] (x : t_Reverse'0) (y : t_Reverse'0) : ()
+  function cmp_gt_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 171 4 171 35] (x : t_Reverse'0) (y : t_Reverse'0) : ()
     
   
   goal vc_cmp_gt_log'0 : [%#scmp0] gt_log'0 x y = (cmp_log'0 x y = C_Greater'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl [#"../../../creusot-contracts/src/std/cmp.rs" 108 4 108 20] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 107 14 107 45
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 105 4 105 10
-  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl [#"../../../creusot-contracts/src/std/cmp.rs" 176 4 176 20] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 175 14 175 45
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 173 4 173 10
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -583,7 +2190,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl [#"../
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -594,16 +2201,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl [#"../
   
   constant x  : t_Reverse'0
   
-  function refl'0 [#"../../../creusot-contracts/src/std/cmp.rs" 108 4 108 20] (x : t_Reverse'0) : ()
+  function refl'0 [#"../../../creusot-contracts/src/std/cmp.rs" 176 4 176 20] (x : t_Reverse'0) : ()
   
   goal vc_refl'0 : [%#scmp0] cmp_log'0 x x = C_Equal'0
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans [#"../../../creusot-contracts/src/std/cmp.rs" 115 4 115 52] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 112 15 112 32
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 113 15 113 32
-  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 114 14 114 31
-  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 110 4 110 10
-  let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans [#"../../../creusot-contracts/src/std/cmp.rs" 183 4 183 52] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 180 15 180 32
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 181 15 181 32
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 182 14 182 31
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 178 4 178 10
+  let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord7 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -679,7 +2286,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans [#"..
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord5] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp4] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -696,16 +2303,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans [#"..
   
   constant o  : t_Ordering'0
   
-  function trans'0 [#"../../../creusot-contracts/src/std/cmp.rs" 115 4 115 52] (x : t_Reverse'0) (y : t_Reverse'0) (z : t_Reverse'0) (o : t_Ordering'0) : ()
+  function trans'0 [#"../../../creusot-contracts/src/std/cmp.rs" 183 4 183 52] (x : t_Reverse'0) (y : t_Reverse'0) (z : t_Reverse'0) (o : t_Ordering'0) : ()
     
   
   goal vc_trans'0 : ([%#scmp1] cmp_log'0 y z = o)  -> ([%#scmp0] cmp_log'0 x y = o)  -> ([%#scmp2] cmp_log'0 x z = o)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1 [#"../../../creusot-contracts/src/std/cmp.rs" 121 4 121 33] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 119 15 119 45
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 120 14 120 47
-  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 117 4 117 10
-  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1 [#"../../../creusot-contracts/src/std/cmp.rs" 189 4 189 33] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 187 15 187 45
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 188 14 188 47
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 185 4 185 10
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -781,7 +2388,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1 [#
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -794,16 +2401,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1 [#
   
   constant y  : t_Reverse'0
   
-  function antisym1'0 [#"../../../creusot-contracts/src/std/cmp.rs" 121 4 121 33] (x : t_Reverse'0) (y : t_Reverse'0) : ()
+  function antisym1'0 [#"../../../creusot-contracts/src/std/cmp.rs" 189 4 189 33] (x : t_Reverse'0) (y : t_Reverse'0) : ()
     
   
   goal vc_antisym1'0 : ([%#scmp0] cmp_log'0 x y = C_Less'0)  -> ([%#scmp1] cmp_log'0 y x = C_Greater'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2 [#"../../../creusot-contracts/src/std/cmp.rs" 127 4 127 33] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 125 15 125 48
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 126 14 126 44
-  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 123 4 123 10
-  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2 [#"../../../creusot-contracts/src/std/cmp.rs" 195 4 195 33] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 193 15 193 48
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 194 14 194 44
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 191 4 191 10
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -879,7 +2486,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2 [#
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -892,15 +2499,15 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2 [#
   
   constant y  : t_Reverse'0
   
-  function antisym2'0 [#"../../../creusot-contracts/src/std/cmp.rs" 127 4 127 33] (x : t_Reverse'0) (y : t_Reverse'0) : ()
+  function antisym2'0 [#"../../../creusot-contracts/src/std/cmp.rs" 195 4 195 33] (x : t_Reverse'0) (y : t_Reverse'0) : ()
     
   
   goal vc_antisym2'0 : ([%#scmp0] cmp_log'0 x y = C_Greater'0)  -> ([%#scmp1] cmp_log'0 y x = C_Less'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp [#"../../../creusot-contracts/src/std/cmp.rs" 132 4 132 31] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 131 14 131 59
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 129 4 129 10
-  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp [#"../../../creusot-contracts/src/std/cmp.rs" 200 4 200 31] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 199 14 199 59
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 197 4 197 10
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -976,7 +2583,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp [#".
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -989,7 +2596,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp [#".
   
   constant y  : t_Reverse'0
   
-  function eq_cmp'0 [#"../../../creusot-contracts/src/std/cmp.rs" 132 4 132 31] (x : t_Reverse'0) (y : t_Reverse'0) : ()
+  function eq_cmp'0 [#"../../../creusot-contracts/src/std/cmp.rs" 200 4 200 31] (x : t_Reverse'0) (y : t_Reverse'0) : ()
   
   goal vc_eq_cmp'0 : [%#scmp0] (x = y) = (cmp_log'0 x y = C_Equal'0)
 end
@@ -17692,10 +19299,10 @@ module M_creusot_contracts__stdqy35z1__vec__qyi12862303518309667396__produces_re
   goal refines : [%#svec0] forall self : t_IntoIter'0 . forall result : () . produces'0 self (Seq.empty  : Seq.seq t_T'0) self
    -> produces'0 self (Seq.empty  : Seq.seq t_T'0) self
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 93 4 93 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 93 4 93 35
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 161 4 161 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 161 4 161 35
   let%span sord1 = "../../../creusot-contracts/src/logic/ord.rs" 36 20 36 53
-  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -17771,7 +19378,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log_
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -17788,9 +19395,9 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log_
   goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . forall result : () . lt_log'0 x y
   = (cmp_log'0 x y = C_Less'0)  -> lt_log'0 x y = (cmp_log'0 x y = C_Less'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1__refines [#"../../../creusot-contracts/src/std/cmp.rs" 121 4 121 33] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 121 4 121 33
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1__refines [#"../../../creusot-contracts/src/std/cmp.rs" 189 4 189 33] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 189 4 189 33
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -17866,7 +19473,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1__r
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord2] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp1] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -17878,9 +19485,9 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1__r
   goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . cmp_log'0 x y = C_Less'0
    -> cmp_log'0 x y = C_Less'0 /\ (forall result : () . cmp_log'0 y x = C_Greater'0  -> cmp_log'0 y x = C_Greater'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp__refines [#"../../../creusot-contracts/src/std/cmp.rs" 132 4 132 31] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 132 4 132 31
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp__refines [#"../../../creusot-contracts/src/std/cmp.rs" 200 4 200 31] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 200 4 200 31
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -17956,7 +19563,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp__ref
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord2] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp1] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -17968,9 +19575,9 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp__ref
   goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . forall result : () . (x = y)
   = (cmp_log'0 x y = C_Equal'0)  -> (x = y) = (cmp_log'0 x y = C_Equal'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl__refines [#"../../../creusot-contracts/src/std/cmp.rs" 108 4 108 20] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 108 4 108 20
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl__refines [#"../../../creusot-contracts/src/std/cmp.rs" 176 4 176 20] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 176 4 176 20
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -18046,7 +19653,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl__refin
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord2] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp1] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -18058,9 +19665,9 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl__refin
   goal refines : [%#scmp0] forall x : t_Reverse'0 . forall result : () . cmp_log'0 x x = C_Equal'0
    -> cmp_log'0 x x = C_Equal'0
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans__refines [#"../../../creusot-contracts/src/std/cmp.rs" 115 4 115 52] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 115 4 115 52
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans__refines [#"../../../creusot-contracts/src/std/cmp.rs" 183 4 183 52] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 183 4 183 52
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -18136,7 +19743,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans__refi
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord2] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp1] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -18150,9 +19757,9 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans__refi
   /\ cmp_log'0 x y = o
    -> cmp_log'0 y z = o /\ cmp_log'0 x y = o /\ (forall result : () . cmp_log'0 x z = o  -> cmp_log'0 x z = o)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2__refines [#"../../../creusot-contracts/src/std/cmp.rs" 127 4 127 33] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 127 4 127 33
-  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2__refines [#"../../../creusot-contracts/src/std/cmp.rs" 195 4 195 33] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 195 4 195 33
+  let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -18228,7 +19835,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2__r
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord2] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp1] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -18240,10 +19847,10 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2__r
   goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . cmp_log'0 x y = C_Greater'0
    -> cmp_log'0 x y = C_Greater'0 /\ (forall result : () . cmp_log'0 y x = C_Less'0  -> cmp_log'0 y x = C_Less'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 88 4 88 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 88 4 88 35
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 156 4 156 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 156 4 156 35
   let%span sord1 = "../../../creusot-contracts/src/logic/ord.rs" 25 20 25 56
-  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -18319,7 +19926,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log_
   
   axiom cmp_le_log'1_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'1 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -18336,10 +19943,10 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log_
   goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . forall result : () . le_log'0 x y
   = (cmp_log'0 x y <> C_Greater'0)  -> le_log'0 x y = (cmp_log'0 x y <> C_Greater'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 98 4 98 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 98 4 98 35
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 166 4 166 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 166 4 166 35
   let%span sord1 = "../../../creusot-contracts/src/logic/ord.rs" 47 20 47 53
-  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -18415,7 +20022,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log_
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
@@ -18432,10 +20039,10 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log_
   goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . forall result : () . ge_log'0 x y
   = (cmp_log'0 x y <> C_Less'0)  -> ge_log'0 x y = (cmp_log'0 x y <> C_Less'0)
 end
-module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 103 4 103 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
-  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 103 4 103 35
+module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 171 4 171 35] (* <std::cmp::Reverse<T> as logic::ord::OrdLogic> *)
+  let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 171 4 171 35
   let%span sord1 = "../../../creusot-contracts/src/logic/ord.rs" 58 20 58 56
-  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 146 8 150 9
   let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -18511,7 +20118,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log_
   
   axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0)
   
-  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
+  function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 145 4 145 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0
     
    =
     [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with
diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml
index e070cf0243..fe7b06734e 100644
--- a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml
+++ b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml
@@ -36,6 +36,56 @@
  </transf>
  </goal>
 </theory>
+<theory name="M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_PartialEq_Rhs_ne_body" proved="true">
+ <goal name="vc_extern_spec_std_cmp_PartialEq_Rhs_ne_body&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.016119" steps="22"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_PartialOrd_Rhs_lt_body" proved="true">
+ <goal name="vc_extern_spec_std_cmp_PartialOrd_Rhs_lt_body&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.015008" steps="23"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_PartialOrd_Rhs_le_body" proved="true">
+ <goal name="vc_extern_spec_std_cmp_PartialOrd_Rhs_le_body&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.016630" steps="18"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_PartialOrd_Rhs_gt_body" proved="true">
+ <goal name="vc_extern_spec_std_cmp_PartialOrd_Rhs_gt_body&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.017854" steps="18"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_PartialOrd_Rhs_ge_body" proved="true">
+ <goal name="vc_extern_spec_std_cmp_PartialOrd_Rhs_ge_body&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.012929" steps="23"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_Ord_max_body" proved="true">
+ <goal name="vc_extern_spec_std_cmp_Ord_max_body&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.016186" steps="59"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_Ord_min_body" proved="true">
+ <goal name="vc_extern_spec_std_cmp_Ord_min_body&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.015223" steps="57"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_Ord_clamp_body" proved="true">
+ <goal name="vc_extern_spec_std_cmp_Ord_clamp_body&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.016058" steps="84"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_max_body" proved="true">
+ <goal name="vc_extern_spec_std_cmp_max_body&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.019050" steps="8"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_min_body" proved="true">
+ <goal name="vc_extern_spec_std_cmp_min_body&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.018598" steps="8"/></proof>
+ </goal>
+</theory>
 <theory name="M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log__refines" proved="true">
  <goal name="refines" proved="true">
  <proof prover="0"><result status="valid" time="0.015481" steps="339"/></proof>
@@ -1656,6 +1706,46 @@
  <proof prover="3"><result status="valid" time="0.012789" steps="10"/></proof>
  </goal>
 </theory>
+<theory name="M_creusot_contracts__resolve__qyi4855891653524509355__resolve_coherence__refines" proved="true">
+ <goal name="refines" proved="true">
+ <proof prover="3"><result status="valid" time="0.019076" steps="2"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__resolve__qyi4855891653524509355__resolve_coherence" proved="true">
+ <goal name="vc_resolve_coherence&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.014517" steps="7"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__resolve__qyi6740873903368268328__resolve_coherence__refines" proved="true">
+ <goal name="refines" proved="true">
+ <proof prover="3"><result status="valid" time="0.022889" steps="2"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__resolve__qyi6740873903368268328__resolve_coherence" proved="true">
+ <goal name="vc_resolve_coherence&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.018922" steps="4"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__resolve__qyi10830812895881240411__resolve_coherence__refines" proved="true">
+ <goal name="refines" proved="true">
+ <proof prover="3"><result status="valid" time="0.017216" steps="2"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__resolve__qyi10830812895881240411__resolve_coherence" proved="true">
+ <goal name="vc_resolve_coherence&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.017321" steps="0"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__resolve__qyi12875730110607858017__resolve_coherence__refines" proved="true">
+ <goal name="refines" proved="true">
+ <proof prover="3"><result status="valid" time="0.014800" steps="4"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__resolve__qyi12875730110607858017__resolve_coherence" proved="true">
+ <goal name="vc_resolve_coherence&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.023377" steps="14"/></proof>
+ </goal>
+</theory>
 <theory name="M_creusot_contracts__stdqy35z1__deque__qyi8367101395671471553__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
  <proof prover="1"><result status="valid" time="0.019727" steps="1419"/></proof>
@@ -2019,46 +2109,6 @@
  <proof prover="3"><result status="valid" time="0.016216" steps="0"/></proof>
  </goal>
 </theory>
-<theory name="M_creusot_contracts__resolve__qyi4855891653524509355__resolve_coherence__refines" proved="true">
- <goal name="refines" proved="true">
- <proof prover="3"><result status="valid" time="0.019076" steps="2"/></proof>
- </goal>
-</theory>
-<theory name="M_creusot_contracts__resolve__qyi4855891653524509355__resolve_coherence" proved="true">
- <goal name="vc_resolve_coherence&#39;0" proved="true">
- <proof prover="3"><result status="valid" time="0.014517" steps="7"/></proof>
- </goal>
-</theory>
-<theory name="M_creusot_contracts__resolve__qyi6740873903368268328__resolve_coherence__refines" proved="true">
- <goal name="refines" proved="true">
- <proof prover="3"><result status="valid" time="0.022889" steps="2"/></proof>
- </goal>
-</theory>
-<theory name="M_creusot_contracts__resolve__qyi6740873903368268328__resolve_coherence" proved="true">
- <goal name="vc_resolve_coherence&#39;0" proved="true">
- <proof prover="3"><result status="valid" time="0.018922" steps="4"/></proof>
- </goal>
-</theory>
-<theory name="M_creusot_contracts__resolve__qyi10830812895881240411__resolve_coherence__refines" proved="true">
- <goal name="refines" proved="true">
- <proof prover="3"><result status="valid" time="0.017216" steps="2"/></proof>
- </goal>
-</theory>
-<theory name="M_creusot_contracts__resolve__qyi10830812895881240411__resolve_coherence" proved="true">
- <goal name="vc_resolve_coherence&#39;0" proved="true">
- <proof prover="3"><result status="valid" time="0.017321" steps="0"/></proof>
- </goal>
-</theory>
-<theory name="M_creusot_contracts__resolve__qyi12875730110607858017__resolve_coherence__refines" proved="true">
- <goal name="refines" proved="true">
- <proof prover="3"><result status="valid" time="0.014800" steps="4"/></proof>
- </goal>
-</theory>
-<theory name="M_creusot_contracts__resolve__qyi12875730110607858017__resolve_coherence" proved="true">
- <goal name="vc_resolve_coherence&#39;0" proved="true">
- <proof prover="3"><result status="valid" time="0.023377" steps="14"/></proof>
- </goal>
-</theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__fuse__qyi10730559947553418603__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
  <proof prover="3"><result status="valid" time="0.024500" steps="2"/></proof>
diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz b/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz
index 5ca92942f8..8d3a27c764 100644
Binary files a/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz and b/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/bdd.coma b/creusot/tests/should_succeed/bdd.coma
index 8850901ada..0f569f14b1 100644
--- a/creusot/tests/should_succeed/bdd.coma
+++ b/creusot/tests/should_succeed/bdd.coma
@@ -3748,7 +3748,7 @@ module M_bdd__qyi11078426090797403070__and [#"bdd.rs" 533 4 533 72] (* Context<'
   let%span sbdd9 = "bdd.rs" 66 37 66 40
   let%span sbdd10 = "bdd.rs" 66 52 66 65
   let%span sbdd11 = "bdd.rs" 61 18 64 9
-  let%span scmp12 = "../../../creusot-contracts/src/std/cmp.rs" 50 26 50 85
+  let%span scmp12 = "../../../creusot-contracts/src/std/cmp.rs" 72 26 72 85
   let%span sbdd13 = "bdd.rs" 471 17 471 21
   let%span sbdd14 = "bdd.rs" 464 15 464 40
   let%span sbdd15 = "bdd.rs" 465 15 465 40
diff --git a/creusot/tests/should_succeed/bug/387.coma b/creusot/tests/should_succeed/bug/387.coma
index 075eaee0d9..0042f85e5a 100644
--- a/creusot/tests/should_succeed/bug/387.coma
+++ b/creusot/tests/should_succeed/bug/387.coma
@@ -22,9 +22,9 @@ end
 module M_387__qyi16446429885017832241__height [#"387.rs" 18 4 18 31] (* Tree *)
   let%span s3870 = "387.rs" 21 69 21 70
   let%span s3871 = "387.rs" 20 26 20 27
-  let%span scmp2 = "../../../../creusot-contracts/src/std/cmp.rs" 53 26 53 66
-  let%span scmp3 = "../../../../creusot-contracts/src/std/cmp.rs" 54 26 54 63
-  let%span scmp4 = "../../../../creusot-contracts/src/std/cmp.rs" 7 0 62 1
+  let%span scmp2 = "../../../../creusot-contracts/src/std/cmp.rs" 75 26 75 66
+  let%span scmp3 = "../../../../creusot-contracts/src/std/cmp.rs" 76 26 76 63
+  let%span scmp4 = "../../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
   let%span snum5 = "../../../../creusot-contracts/src/std/num.rs" 21 28 21 33
   
   use prelude.prelude.UInt32
diff --git a/creusot/tests/should_succeed/heapsort_generic.coma b/creusot/tests/should_succeed/heapsort_generic.coma
index 82e61416dc..224550a748 100644
--- a/creusot/tests/should_succeed/heapsort_generic.coma
+++ b/creusot/tests/should_succeed/heapsort_generic.coma
@@ -141,8 +141,8 @@ module M_heapsort_generic__sift_down [#"heapsort_generic.rs" 41 0 43 29]
   let%span sseq28 = "../../../creusot-contracts/src/logic/seq.rs" 316 8 316 41
   let%span svec29 = "../../../creusot-contracts/src/std/vec.rs" 162 27 162 46
   let%span svec30 = "../../../creusot-contracts/src/std/vec.rs" 163 26 163 54
-  let%span scmp31 = "../../../creusot-contracts/src/std/cmp.rs" 33 26 33 76
-  let%span scmp32 = "../../../creusot-contracts/src/std/cmp.rs" 36 26 36 77
+  let%span scmp31 = "../../../creusot-contracts/src/std/cmp.rs" 35 26 35 76
+  let%span scmp32 = "../../../creusot-contracts/src/std/cmp.rs" 43 26 43 77
   let%span svec33 = "../../../creusot-contracts/src/std/vec.rs" 175 26 175 42
   let%span svec34 = "../../../creusot-contracts/src/std/vec.rs" 176 26 176 48
   let%span sslice35 = "../../../creusot-contracts/src/std/slice.rs" 257 19 257 35
diff --git a/creusot/tests/should_succeed/instant.coma b/creusot/tests/should_succeed/instant.coma
index 450293ef21..8bf92b98ea 100644
--- a/creusot/tests/should_succeed/instant.coma
+++ b/creusot/tests/should_succeed/instant.coma
@@ -22,7 +22,7 @@ module M_instant__test_instant [#"instant.rs" 7 0 7 21]
   let%span stime20 = "../../../creusot-contracts/src/std/time.rs" 156 26 156 38
   let%span stime21 = "../../../creusot-contracts/src/std/time.rs" 82 26 82 57
   let%span stime22 = "../../../creusot-contracts/src/std/time.rs" 159 26 159 38
-  let%span scmp23 = "../../../creusot-contracts/src/std/cmp.rs" 42 26 42 77
+  let%span scmp23 = "../../../creusot-contracts/src/std/cmp.rs" 59 26 59 77
   let%span stime24 = "../../../creusot-contracts/src/std/time.rs" 178 26 178 79
   let%span stime25 = "../../../creusot-contracts/src/std/time.rs" 179 26 179 95
   let%span soption26 = "../../../creusot-contracts/src/std/option.rs" 31 0 423 1
@@ -35,7 +35,7 @@ module M_instant__test_instant [#"instant.rs" 7 0 7 21]
   let%span stime33 = "../../../creusot-contracts/src/std/time.rs" 215 18 215 48
   let%span stime34 = "../../../creusot-contracts/src/std/time.rs" 216 18 216 46
   let%span stime35 = "../../../creusot-contracts/src/std/time.rs" 191 0 226 1
-  let%span scmp36 = "../../../creusot-contracts/src/std/cmp.rs" 39 26 39 76
+  let%span scmp36 = "../../../creusot-contracts/src/std/cmp.rs" 51 26 51 76
   let%span stime37 = "../../../creusot-contracts/src/std/time.rs" 72 0 189 1
   let%span soption38 = "../../../creusot-contracts/src/std/option.rs" 36 26 36 51
   let%span soption39 = "../../../creusot-contracts/src/std/option.rs" 51 26 51 51
diff --git a/creusot/tests/should_succeed/ord_trait.coma b/creusot/tests/should_succeed/ord_trait.coma
index 5b4291dbad..305b2a6517 100644
--- a/creusot/tests/should_succeed/ord_trait.coma
+++ b/creusot/tests/should_succeed/ord_trait.coma
@@ -1,7 +1,7 @@
 module M_ord_trait__x [#"ord_trait.rs" 5 0 7 29]
   let%span sord_trait0 = "ord_trait.rs" 5 29 5 30
   let%span sord_trait1 = "ord_trait.rs" 4 10 4 24
-  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 36 26 36 77
+  let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 43 26 43 77
   let%span smodel3 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
   let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
@@ -129,7 +129,7 @@ module M_ord_trait__gt_or_le [#"ord_trait.rs" 13 0 15 29]
   let%span sord_trait0 = "ord_trait.rs" 13 36 13 37
   let%span sord_trait1 = "ord_trait.rs" 13 43 13 44
   let%span sord_trait2 = "ord_trait.rs" 12 10 12 60
-  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 42 26 42 77
+  let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 59 26 59 77
   let%span smodel4 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
   let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
diff --git a/creusot/tests/should_succeed/red_black_tree.coma b/creusot/tests/should_succeed/red_black_tree.coma
index 1059f4a6b0..4bfe8de61f 100644
--- a/creusot/tests/should_succeed/red_black_tree.coma
+++ b/creusot/tests/should_succeed/red_black_tree.coma
@@ -4410,7 +4410,7 @@ module M_red_black_tree__qyi2476155906044564626__insert_rec [#"red_black_tree.rs
   let%span sred_black_tree7 = "red_black_tree.rs" 614 14 615 39
   let%span sred_black_tree8 = "red_black_tree.rs" 616 14 616 56
   let%span sred_black_tree9 = "red_black_tree.rs" 617 14 617 125
-  let%span scmp10 = "../../../creusot-contracts/src/std/cmp.rs" 50 26 50 85
+  let%span scmp10 = "../../../creusot-contracts/src/std/cmp.rs" 72 26 72 85
   let%span sred_black_tree11 = "red_black_tree.rs" 534 20 534 24
   let%span sred_black_tree12 = "red_black_tree.rs" 515 15 515 43
   let%span sred_black_tree13 = "red_black_tree.rs" 516 15 517 45
@@ -6589,7 +6589,7 @@ module M_red_black_tree__qyi2476155906044564626__delete_rec [#"red_black_tree.rs
   let%span soption14 = "../../../creusot-contracts/src/std/option.rs" 31 0 423 1
   let%span sboxed15 = "../../../creusot-contracts/src/std/boxed.rs" 43 26 43 43
   let%span sboxed16 = "../../../creusot-contracts/src/std/boxed.rs" 44 26 44 43
-  let%span scmp17 = "../../../creusot-contracts/src/std/cmp.rs" 50 26 50 85
+  let%span scmp17 = "../../../creusot-contracts/src/std/cmp.rs" 72 26 72 85
   let%span sred_black_tree18 = "red_black_tree.rs" 412 15 412 19
   let%span sred_black_tree19 = "red_black_tree.rs" 411 14 411 45
   let%span sred_black_tree20 = "red_black_tree.rs" 436 25 436 29
@@ -10638,7 +10638,7 @@ module M_red_black_tree__qyi1501420612169366910__get [#"red_black_tree.rs" 889 4
   let%span smodel11 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
   let%span sred_black_tree12 = "red_black_tree.rs" 37 12 41 13
   let%span sred_black_tree13 = "red_black_tree.rs" 235 12 241 13
-  let%span scmp14 = "../../../creusot-contracts/src/std/cmp.rs" 50 26 50 85
+  let%span scmp14 = "../../../creusot-contracts/src/std/cmp.rs" 72 26 72 85
   let%span smodel15 = "../../../creusot-contracts/src/model.rs" 92 8 92 22
   let%span sred_black_tree16 = "red_black_tree.rs" 170 20 170 54
   let%span sred_black_tree17 = "red_black_tree.rs" 67 14 68 91
@@ -11081,7 +11081,7 @@ module M_red_black_tree__qyi1501420612169366910__get_mut [#"red_black_tree.rs" 9
   let%span smodel25 = "../../../creusot-contracts/src/model.rs" 83 8 83 28
   let%span sred_black_tree26 = "red_black_tree.rs" 235 12 241 13
   let%span sred_black_tree27 = "red_black_tree.rs" 297 12 303 13
-  let%span scmp28 = "../../../creusot-contracts/src/std/cmp.rs" 50 26 50 85
+  let%span scmp28 = "../../../creusot-contracts/src/std/cmp.rs" 72 26 72 85
   let%span smodel29 = "../../../creusot-contracts/src/model.rs" 110 8 110 22
   let%span sred_black_tree30 = "red_black_tree.rs" 761 20 761 27
   let%span sred_black_tree31 = "red_black_tree.rs" 170 20 170 54
diff --git a/creusot/tests/should_succeed/selection_sort_generic.coma b/creusot/tests/should_succeed/selection_sort_generic.coma
index c56319652c..4efd70dba4 100644
--- a/creusot/tests/should_succeed/selection_sort_generic.coma
+++ b/creusot/tests/should_succeed/selection_sort_generic.coma
@@ -31,7 +31,7 @@ module M_selection_sort_generic__selection_sort [#"selection_sort_generic.rs" 30
   let%span siter29 = "../../../creusot-contracts/src/std/iter.rs" 103 26 106 17
   let%span svec30 = "../../../creusot-contracts/src/std/vec.rs" 162 27 162 46
   let%span svec31 = "../../../creusot-contracts/src/std/vec.rs" 163 26 163 54
-  let%span scmp32 = "../../../creusot-contracts/src/std/cmp.rs" 33 26 33 76
+  let%span scmp32 = "../../../creusot-contracts/src/std/cmp.rs" 35 26 35 76
   let%span svec33 = "../../../creusot-contracts/src/std/vec.rs" 175 26 175 42
   let%span svec34 = "../../../creusot-contracts/src/std/vec.rs" 176 26 176 48
   let%span sslice35 = "../../../creusot-contracts/src/std/slice.rs" 257 19 257 35
diff --git a/creusot/tests/should_succeed/syntax/10_mutual_rec_types.coma b/creusot/tests/should_succeed/syntax/10_mutual_rec_types.coma
index ef5f8e1c0c..8056679c69 100644
--- a/creusot/tests/should_succeed/syntax/10_mutual_rec_types.coma
+++ b/creusot/tests/should_succeed/syntax/10_mutual_rec_types.coma
@@ -22,9 +22,9 @@ end
 module M_10_mutual_rec_types__qyi18211245992252154719__height [#"10_mutual_rec_types.rs" 18 4 18 31] (* Tree *)
   let%span s10_mutual_rec_types0 = "10_mutual_rec_types.rs" 21 69 21 70
   let%span s10_mutual_rec_types1 = "10_mutual_rec_types.rs" 20 26 20 27
-  let%span scmp2 = "../../../../creusot-contracts/src/std/cmp.rs" 53 26 53 66
-  let%span scmp3 = "../../../../creusot-contracts/src/std/cmp.rs" 54 26 54 63
-  let%span scmp4 = "../../../../creusot-contracts/src/std/cmp.rs" 7 0 62 1
+  let%span scmp2 = "../../../../creusot-contracts/src/std/cmp.rs" 75 26 75 66
+  let%span scmp3 = "../../../../creusot-contracts/src/std/cmp.rs" 76 26 76 63
+  let%span scmp4 = "../../../../creusot-contracts/src/std/cmp.rs" 7 0 130 1
   let%span snum5 = "../../../../creusot-contracts/src/std/num.rs" 21 28 21 33
   
   use prelude.prelude.UInt32
diff --git a/creusot/tests/should_succeed/vector/02_gnome.coma b/creusot/tests/should_succeed/vector/02_gnome.coma
index d40bb2e872..abef160bf1 100644
--- a/creusot/tests/should_succeed/vector/02_gnome.coma
+++ b/creusot/tests/should_succeed/vector/02_gnome.coma
@@ -19,7 +19,7 @@ module M_02_gnome__gnome_sort [#"02_gnome.rs" 22 0 24 29]
   let%span svec17 = "../../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span svec18 = "../../../../creusot-contracts/src/std/vec.rs" 162 27 162 46
   let%span svec19 = "../../../../creusot-contracts/src/std/vec.rs" 163 26 163 54
-  let%span scmp20 = "../../../../creusot-contracts/src/std/cmp.rs" 36 26 36 77
+  let%span scmp20 = "../../../../creusot-contracts/src/std/cmp.rs" 43 26 43 77
   let%span svec21 = "../../../../creusot-contracts/src/std/vec.rs" 175 26 175 42
   let%span svec22 = "../../../../creusot-contracts/src/std/vec.rs" 176 26 176 48
   let%span sslice23 = "../../../../creusot-contracts/src/std/slice.rs" 257 19 257 35
diff --git a/creusot/tests/should_succeed/vector/05_binary_search_generic.coma b/creusot/tests/should_succeed/vector/05_binary_search_generic.coma
index ba29fab685..b91900894a 100644
--- a/creusot/tests/should_succeed/vector/05_binary_search_generic.coma
+++ b/creusot/tests/should_succeed/vector/05_binary_search_generic.coma
@@ -21,8 +21,8 @@ module M_05_binary_search_generic__binary_search [#"05_binary_search_generic.rs"
   let%span smodel19 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28
   let%span svec20 = "../../../../creusot-contracts/src/std/vec.rs" 162 27 162 46
   let%span svec21 = "../../../../creusot-contracts/src/std/vec.rs" 163 26 163 54
-  let%span scmp22 = "../../../../creusot-contracts/src/std/cmp.rs" 39 26 39 76
-  let%span scmp23 = "../../../../creusot-contracts/src/std/cmp.rs" 50 26 50 85
+  let%span scmp22 = "../../../../creusot-contracts/src/std/cmp.rs" 51 26 51 76
+  let%span scmp23 = "../../../../creusot-contracts/src/std/cmp.rs" 72 26 72 85
   let%span s05_binary_search_generic24 = "05_binary_search_generic.rs" 17 4 17 31
   let%span svec25 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span svec26 = "../../../../creusot-contracts/src/std/vec.rs" 29 14 29 47