diff --git a/creusot-contracts-proc/src/pretyping.rs b/creusot-contracts-proc/src/pretyping.rs
index aebacac969..b519da573a 100644
--- a/creusot-contracts-proc/src/pretyping.rs
+++ b/creusot-contracts-proc/src/pretyping.rs
@@ -59,16 +59,16 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
                     Ok(quote_spanned! {sp=> ::creusot_contracts::__stubs::neq(#left, #right) })
                 }
                 Lt(_) => Ok(
-                    quote_spanned! {sp=> ::creusot_contracts::logic::OrdLogic::lt_log(#left, #right) },
+                    quote_spanned! {sp=> ::creusot_contracts::logic::PartialOrdLogic::lt_log(#left, #right) },
                 ),
                 Le(_) => Ok(
-                    quote_spanned! {sp=> ::creusot_contracts::logic::OrdLogic::le_log(#left, #right) },
+                    quote_spanned! {sp=> ::creusot_contracts::logic::PartialOrdLogic::le_log(#left, #right) },
                 ),
                 Ge(_) => Ok(
-                    quote_spanned! {sp=> ::creusot_contracts::logic::OrdLogic::ge_log(#left, #right) },
+                    quote_spanned! {sp=> ::creusot_contracts::logic::PartialOrdLogic::ge_log(#left, #right) },
                 ),
                 Gt(_) => Ok(
-                    quote_spanned! {sp=> ::creusot_contracts::logic::OrdLogic::gt_log(#left, #right) },
+                    quote_spanned! {sp=> ::creusot_contracts::logic::PartialOrdLogic::gt_log(#left, #right) },
                 ),
                 _ => Ok(quote_spanned! {sp=> #left #op #right }),
             }
diff --git a/creusot-contracts/src/lib.rs b/creusot-contracts/src/lib.rs
index ca8e26b8df..67de1f8e4b 100644
--- a/creusot-contracts/src/lib.rs
+++ b/creusot-contracts/src/lib.rs
@@ -175,7 +175,7 @@ pub mod well_founded;
 // We add some common things at the root of the creusot-contracts library
 pub use crate::{
     ghost::Ghost,
-    logic::{Int, OrdLogic, Seq},
+    logic::{Int, PartialOrdLogic, OrdLogic, Seq},
     macros::*,
     model::{DeepModel, ShallowModel},
     resolve::Resolve,
diff --git a/creusot-contracts/src/logic.rs b/creusot-contracts/src/logic.rs
index 568ed21121..6d0c22d944 100644
--- a/creusot-contracts/src/logic.rs
+++ b/creusot-contracts/src/logic.rs
@@ -14,6 +14,6 @@ pub use fset::FSet;
 pub use int::Int;
 pub use mapping::Mapping;
 pub use ops::IndexLogic;
-pub use ord::OrdLogic;
+pub use ord::{PartialOrdLogic, OrdLogic};
 pub use seq::Seq;
 pub use set::Set;
diff --git a/creusot-contracts/src/logic/ord.rs b/creusot-contracts/src/logic/ord.rs
index 4b6fcf1db0..7b33c76851 100644
--- a/creusot-contracts/src/logic/ord.rs
+++ b/creusot-contracts/src/logic/ord.rs
@@ -1,157 +1,144 @@
-use crate::{std::cmp::Ordering, *};
+use crate::{std::cmp::Ordering, util::*, *};
 
 #[allow(unused)]
-pub trait OrdLogic {
-    #[logic]
-    fn cmp_log(self, _: Self) -> Ordering;
-
+pub trait PartialOrdLogic {
     #[predicate]
-    fn le_log(self, o: Self) -> bool {
-        pearlite! { self.cmp_log(o) != Ordering::Greater }
-    }
+    fn lt_log(self, _: Self) -> bool;
 
     #[law]
-    #[ensures(x.le_log(y) == (x.cmp_log(y) != Ordering::Greater))]
-    fn cmp_le_log(x: Self, y: Self);
+    #[ensures(!self.lt_log(self))]
+    fn lt_log_irrefl(self);
 
-    #[predicate]
-    fn lt_log(self, o: Self) -> bool {
-        pearlite! { self.cmp_log(o) == Ordering::Less }
-    }
+    #[law]
+    #[requires(x.lt_log(y))]
+    #[ensures(!y.lt_log(x))]
+    fn lt_log_asymm(x: Self, y: Self);
 
     #[law]
-    #[ensures(x.lt_log(y) == (x.cmp_log(y) == Ordering::Less))]
-    fn cmp_lt_log(x: Self, y: Self);
+    #[requires(x.lt_log(y))]
+    #[requires(y.lt_log(z))]
+    #[ensures(x.lt_log(z))]
+    fn lt_log_trans(x: Self, y: Self, z: Self);
 
     #[predicate]
-    fn ge_log(self, o: Self) -> bool {
-        pearlite! { self.cmp_log(o) != Ordering::Less }
+    #[ensures(result == other.lt_log(self))]
+    fn gt_log(self, other: Self) -> bool {
+        other.lt_log(self)
     }
 
-    #[law]
-    #[ensures(x.ge_log(y) == (x.cmp_log(y) != Ordering::Less))]
-    fn cmp_ge_log(x: Self, y: Self);
-
     #[predicate]
-    fn gt_log(self, o: Self) -> bool {
-        pearlite! { self.cmp_log(o) == Ordering::Greater }
+    #[ensures(result == (self.lt_log(other) || self == other))]
+    fn le_log(self, other: Self) -> bool {
+        self.lt_log(other) || self == other
     }
 
     #[law]
-    #[ensures(x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater))]
-    fn cmp_gt_log(x: Self, y: Self);
+    #[ensures(self.le_log(self))]
+    fn le_log_refl(self) {}
 
     #[law]
-    #[ensures(x.cmp_log(x) == Ordering::Equal)]
-    fn refl(x: Self);
+    #[requires(x.le_log(y))]
+    #[requires(y.le_log(x))]
+    #[ensures(x == y)]
+    fn le_log_anti(x: Self, y: Self) {
+        Self::lt_log_asymm(x, y)
+    }
 
     #[law]
-    #[requires(x.cmp_log(y) == o)]
-    #[requires(y.cmp_log(z) == o)]
-    #[ensures(x.cmp_log(z) == o)]
-    fn trans(x: Self, y: Self, z: Self, o: Ordering);
+    #[requires(x.le_log(y))]
+    #[requires(y.le_log(z))]
+    #[ensures(x.le_log(z))]
+    fn le_log_trans(x: Self, y: Self, z: Self) {
+        Self::lt_log_trans(x, y, z);
+    }
 
-    #[law]
-    #[requires(x.cmp_log(y) == Ordering::Less)]
-    #[ensures(y.cmp_log(x) == Ordering::Greater)]
-    fn antisym1(x: Self, y: Self);
+    #[predicate]
+    #[ensures(result == other.le_log(self))]
+    fn ge_log(self, other: Self) -> bool {
+        other.le_log(self)
+    }
 
-    #[law]
-    #[requires(x.cmp_log(y) == Ordering::Greater)]
-    #[ensures(y.cmp_log(x) == Ordering::Less)]
-    fn antisym2(x: Self, y: Self);
+    #[logic]
+    #[ensures((result == Some(Ordering::Less)) == self.lt_log(other))]
+    #[ensures((result == Some(Ordering::Equal)) == (self == other))]
+    #[ensures((result == Some(Ordering::Greater)) == self.gt_log(other))]
+    fn partial_cmp_log(self, other: Self) -> Option<Ordering> {
+        Self::lt_log_asymm(self, other);
+
+        if self.lt_log(other) {
+            Some(Ordering::Less)
+        } else if self == other {
+            Some(Ordering::Equal)
+        } else if other.lt_log(self) {
+            Some(Ordering::Greater)
+        } else {
+            None
+        }
+    }
+}
+
+#[allow(unused)]
+pub trait OrdLogic: PartialOrdLogic {
+    #[logic]
+    #[ensures(self.partial_cmp_log(other) == Some(result))]
+    fn cmp_log(self, other: Self) -> Ordering {
+        Self::trichotomy(self, other);
+
+        unwrap(self.partial_cmp_log(other))
+    }
 
     #[law]
-    #[ensures((x == y) == (x.cmp_log(y) == Ordering::Equal))]
-    fn eq_cmp(x: Self, y: Self);
+    #[ensures(x.lt_log(y) || x == y || y.lt_log(x))]
+    fn trichotomy(x: Self, y: Self);
 }
 
 macro_rules! ord_logic_impl {
     ($t:ty) => {
-        impl OrdLogic for $t {
-            #[logic]
-            fn cmp_log(self, o: Self) -> Ordering {
-                if self < o {
-                    Ordering::Less
-                } else if self == o {
-                    Ordering::Equal
-                } else {
-                    Ordering::Greater
-                }
-            }
-
-            #[trusted]
-            #[predicate]
-            #[creusot::builtins = "int.Int.(<=)"]
-            fn le_log(self, _: Self) -> bool {
-                true
-            }
-
-            #[trusted]
+        impl PartialOrdLogic for $t {
             #[predicate]
             #[creusot::builtins = "int.Int.(<)"]
             fn lt_log(self, _: Self) -> bool {
-                true
+                pearlite! { absurd }
             }
 
-            #[trusted]
             #[predicate]
-            #[creusot::builtins = "int.Int.(>=)"]
-            fn ge_log(self, _: Self) -> bool {
-                true
+            #[creusot::builtins = "int.Int.(<=)"]
+            fn le_log(self, _: Self) -> bool {
+                pearlite! { absurd }
             }
 
-            #[trusted]
             #[predicate]
             #[creusot::builtins = "int.Int.(>)"]
             fn gt_log(self, _: Self) -> bool {
-                true
-            }
-
-            #[logic]
-            fn cmp_le_log(_: Self, _: Self) {
-                ()
-            }
-
-            #[logic]
-            fn cmp_lt_log(_: Self, _: Self) {
-                ()
+                pearlite! { absurd }
             }
 
-            #[logic]
-            fn cmp_ge_log(_: Self, _: Self) {
-                ()
-            }
-
-            #[logic]
-            fn cmp_gt_log(_: Self, _: Self) {
-                ()
+            #[predicate]
+            #[creusot::builtins = "int.Int.(>=)"]
+            fn ge_log(self, _: Self) -> bool {
+                pearlite! { absurd }
             }
 
-            #[logic]
-            fn refl(_: Self) {
-                ()
-            }
+            #[law]
+            #[ensures(!self.lt_log(self))]
+            fn lt_log_irrefl(self) {}
 
-            #[logic]
-            fn trans(_: Self, _: Self, _: Self, _: Ordering) {
-                ()
-            }
+            #[law]
+            #[requires(x.lt_log(y))]
+            #[ensures(!y.lt_log(x))]
+            fn lt_log_asymm(x: Self, y: Self) {}
 
-            #[logic]
-            fn antisym1(_: Self, _: Self) {
-                ()
-            }
-
-            #[logic]
-            fn antisym2(_: Self, _: Self) {
-                ()
-            }
+            #[law]
+            #[requires(x.lt_log(y))]
+            #[requires(y.lt_log(z))]
+            #[ensures(x.lt_log(z))]
+            fn lt_log_trans(x: Self, y: Self, z: Self) {}
+        }
 
-            #[logic]
-            fn eq_cmp(_: Self, _: Self) {
-                ()
-            }
+        impl OrdLogic for $t {
+            #[law]
+            #[ensures(x.lt_log(y) || x == y || y.lt_log(x))]
+            fn trichotomy(x: Self, y: Self) {}
         }
     };
 }
@@ -172,115 +159,71 @@ ord_logic_impl!(i64);
 ord_logic_impl!(i128);
 ord_logic_impl!(isize);
 
-impl<A: OrdLogic, B: OrdLogic> OrdLogic for (A, B) {
-    #[logic]
-    fn cmp_log(self, o: Self) -> Ordering {
-        pearlite! { {
-            let r = self.0.cmp_log(o.0);
-            if r == Ordering::Equal {
-                self.1.cmp_log(o.1)
-            } else {
-                r
-            }
-        } }
-    }
-
-    #[predicate]
-    fn le_log(self, o: Self) -> bool {
-        pearlite! { (self.0 == o.0 && self.1 <= o.1) || self.0 <= o.0 }
-    }
-
-    #[logic]
-    fn cmp_le_log(_: Self, _: Self) {}
-
-    #[predicate]
-    fn lt_log(self, o: Self) -> bool {
-        pearlite! { (self.0 == o.0 && self.1 < o.1) || self.0 < o.0 }
-    }
-
-    #[logic]
-    fn cmp_lt_log(_: Self, _: Self) {}
-
-    #[predicate]
-    fn ge_log(self, o: Self) -> bool {
-        pearlite! { (self.0 == o.0 && self.1 >= o.1) || self.0 >= o.0 }
-    }
-
-    #[logic]
-    fn cmp_ge_log(_: Self, _: Self) {}
-
+impl<A: PartialOrdLogic, B: PartialOrdLogic> PartialOrdLogic for (A, B) {
     #[predicate]
-    fn gt_log(self, o: Self) -> bool {
-        pearlite! { (self.0 == o.0 && self.1 > o.1) || self.0 > o.0 }
-    }
-
-    #[logic]
-    fn cmp_gt_log(_: Self, _: Self) {}
-
-    #[logic]
-    fn refl(_: Self) {}
-
-    #[logic]
-    fn trans(_: Self, _: Self, _: Self, _: Ordering) {}
-
-    #[logic]
-    fn antisym1(_: Self, _: Self) {}
-
-    #[logic]
-    fn antisym2(_: Self, _: Self) {}
-
-    #[logic]
-    fn eq_cmp(_: Self, _: Self) {}
-}
-
-impl<T: OrdLogic> OrdLogic for Option<T> {
-    #[logic]
-    fn cmp_log(self, o: Self) -> Ordering {
-        match (self, o) {
-            (None, None) => Ordering::Equal,
-            (None, Some(_)) => Ordering::Less,
-            (Some(_), None) => Ordering::Greater,
-            (Some(x), Some(y)) => x.cmp_log(y),
-        }
+    fn lt_log(self, other: Self) -> bool {
+        self.0.lt_log(other.0) || (self.0 == other.0 && self.1.lt_log(other.1))
     }
 
     #[law]
-    #[ensures(x.le_log(y) == (x.cmp_log(y) != Ordering::Greater))]
-    fn cmp_le_log(x: Self, y: Self) {}
+    #[ensures(!self.lt_log(self))]
+    fn lt_log_irrefl(self) {}
 
     #[law]
-    #[ensures(x.lt_log(y) == (x.cmp_log(y) == Ordering::Less))]
-    fn cmp_lt_log(x: Self, y: Self) {}
+    #[requires(x.lt_log(y))]
+    #[ensures(!y.lt_log(x))]
+    fn lt_log_asymm(x: Self, y: Self) {}
 
     #[law]
-    #[ensures(x.ge_log(y) == (x.cmp_log(y) != Ordering::Less))]
-    fn cmp_ge_log(x: Self, y: Self) {}
+    #[requires(x.lt_log(y))]
+    #[requires(y.lt_log(z))]
+    #[ensures(x.lt_log(z))]
+    fn lt_log_trans(x: Self, y: Self, z: Self) {}
+}
 
+impl<A: OrdLogic, B: OrdLogic> OrdLogic for (A, B) {
     #[law]
-    #[ensures(x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater))]
-    fn cmp_gt_log(x: Self, y: Self) {}
+    #[ensures(x.lt_log(y) || x == y || y.lt_log(x))]
+    fn trichotomy(x: Self, y: Self) {
+        A::trichotomy(x.0, y.0);
+        B::trichotomy(x.1, y.1);
+    }
+}
 
-    #[law]
-    #[ensures(x.cmp_log(x) == Ordering::Equal)]
-    fn refl(x: Self) {}
+impl<T: PartialOrdLogic> PartialOrdLogic for Option<T> {
+    #[predicate]
+    fn lt_log(self, other: Self) -> bool {
+        match (self, other) {
+            (None, Some(_)) => true,
+            (Some(x), Some(y)) => x.lt_log(y),
+            _ => false,
+        }
+    }
 
     #[law]
-    #[requires(x.cmp_log(y) == o)]
-    #[requires(y.cmp_log(z) == o)]
-    #[ensures(x.cmp_log(z) == o)]
-    fn trans(x: Self, y: Self, z: Self, o: Ordering) {}
+    #[ensures(!self.lt_log(self))]
+    fn lt_log_irrefl(self) {}
 
     #[law]
-    #[requires(x.cmp_log(y) == Ordering::Less)]
-    #[ensures(y.cmp_log(x) == Ordering::Greater)]
-    fn antisym1(x: Self, y: Self) {}
+    #[requires(x.lt_log(y))]
+    #[ensures(!y.lt_log(x))]
+    fn lt_log_asymm(x: Self, y: Self) {}
 
     #[law]
-    #[requires(x.cmp_log(y) == Ordering::Greater)]
-    #[ensures(y.cmp_log(x) == Ordering::Less)]
-    fn antisym2(x: Self, y: Self) {}
+    #[requires(x.lt_log(y))]
+    #[requires(y.lt_log(z))]
+    #[ensures(x.lt_log(z))]
+    fn lt_log_trans(x: Self, y: Self, z: Self) {}
+}
 
+impl<T: OrdLogic> OrdLogic for Option<T> {
     #[law]
-    #[ensures((x == y) == (x.cmp_log(y) == Ordering::Equal))]
-    fn eq_cmp(x: Self, y: Self) {}
+    #[ensures(x.lt_log(y) || x == y || y.lt_log(x))]
+    fn trichotomy(x: Self, y: Self) {
+        match (x, y) {
+            (Some(x), Some(y)) => T::trichotomy(x, y),
+            _ => (),
+        }
+    }
 }
+
diff --git a/creusot-contracts/src/std/cmp.rs b/creusot-contracts/src/std/cmp.rs
index cbaa92c02d..9e3f34ab96 100644
--- a/creusot-contracts/src/std/cmp.rs
+++ b/creusot-contracts/src/std/cmp.rs
@@ -1,4 +1,4 @@
-use crate::{logic::OrdLogic, *};
+use crate::{logic::{PartialOrdLogic, OrdLogic}, *};
 pub use ::std::cmp::*;
 
 #[cfg(creusot)]
@@ -15,14 +15,13 @@ extern_spec! {
                     Rhs: DeepModel<DeepModelTy = Self::DeepModelTy>;
             }
 
-            // TODO: for now, we only support total orders
             trait PartialOrd<Rhs>
                 where Self: DeepModel,
-                      Rhs: DeepModel<DeepModelTy = Self::DeepModelTy>,
-                      Self::DeepModelTy: OrdLogic
+                      Rhs: ?Sized + DeepModel<DeepModelTy = Self::DeepModelTy>,
+                      Self::DeepModelTy: PartialOrdLogic
             {
-                #[ensures(result == Some((*self).deep_model().cmp_log((*rhs).deep_model())))]
-                fn partial_cmp(&self, rhs: &Rhs) -> Option<Ordering>;
+                #[ensures(result == self.deep_model().partial_cmp_log(other.deep_model()))]
+                fn partial_cmp(&self, other: &Rhs) -> Option<Ordering>;
 
                 #[ensures(result == (self.deep_model() < other.deep_model()))]
                 fn lt(&self, other: &Rhs) -> bool;
@@ -38,10 +37,10 @@ extern_spec! {
             }
 
             trait Ord
-                where Self: DeepModel,
+                where Self: DeepModel + PartialOrd<Self>,
                       Self::DeepModelTy: OrdLogic
             {
-                #[ensures(result == (*self).deep_model().cmp_log((*rhs).deep_model()))]
+                #[ensures(result == self.deep_model().cmp_log(rhs.deep_model()))]
                 fn cmp(&self, rhs: &Self) -> Ordering;
 
                 #[ensures(result.deep_model() >= self.deep_model())]
@@ -64,53 +63,32 @@ impl<T: DeepModel> DeepModel for Reverse<T> {
     }
 }
 
-impl<T: OrdLogic> OrdLogic for Reverse<T> {
-    #[logic]
-    fn cmp_log(self, o: Self) -> Ordering {
-        match self.0.cmp_log(o.0) {
-            Ordering::Equal => Ordering::Equal,
-            Ordering::Less => Ordering::Greater,
-            Ordering::Greater => Ordering::Less,
-        }
+impl<T: PartialOrdLogic> PartialOrdLogic for Reverse<T> {
+    #[predicate]
+    fn lt_log(self, other: Self) -> bool {
+        self.0.gt_log(other.0)
     }
 
     #[law]
-    #[ensures(x.le_log(y) == (x.cmp_log(y) != Ordering::Greater))]
-    fn cmp_le_log(x: Self, y: Self) {}
-
-    #[law]
-    #[ensures(x.lt_log(y) == (x.cmp_log(y) == Ordering::Less))]
-    fn cmp_lt_log(x: Self, y: Self) {}
-
-    #[law]
-    #[ensures(x.ge_log(y) == (x.cmp_log(y) != Ordering::Less))]
-    fn cmp_ge_log(x: Self, y: Self) {}
+    #[ensures(!self.lt_log(self))]
+    fn lt_log_irrefl(self) {}
 
     #[law]
-    #[ensures(x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater))]
-    fn cmp_gt_log(x: Self, y: Self) {}
+    #[requires(x.lt_log(y))]
+    #[ensures(!y.lt_log(x))]
+    fn lt_log_asymm(x: Self, y: Self) {}
 
     #[law]
-    #[ensures(x.cmp_log(x) == Ordering::Equal)]
-    fn refl(x: Self) {}
-
-    #[law]
-    #[requires(x.cmp_log(y) == o)]
-    #[requires(y.cmp_log(z) == o)]
-    #[ensures(x.cmp_log(z) == o)]
-    fn trans(x: Self, y: Self, z: Self, o: Ordering) {}
-
-    #[law]
-    #[requires(x.cmp_log(y) == Ordering::Less)]
-    #[ensures(y.cmp_log(x) == Ordering::Greater)]
-    fn antisym1(x: Self, y: Self) {}
-
-    #[law]
-    #[requires(x.cmp_log(y) == Ordering::Greater)]
-    #[ensures(y.cmp_log(x) == Ordering::Less)]
-    fn antisym2(x: Self, y: Self) {}
+    #[requires(x.lt_log(y))]
+    #[requires(y.lt_log(z))]
+    #[ensures(x.lt_log(z))]
+    fn lt_log_trans(x: Self, y: Self, z: Self) {}
+}
 
+impl<T: OrdLogic> OrdLogic for Reverse<T> {
     #[law]
-    #[ensures((x == y) == (x.cmp_log(y) == Ordering::Equal))]
-    fn eq_cmp(x: Self, y: Self) {}
+    #[ensures(x.lt_log(y) || x == y || y.lt_log(x))]
+    fn trichotomy(x: Self, y: Self) {
+        T::trichotomy(y.0, x.0)
+    }
 }
diff --git a/creusot/tests/should_succeed/constrained_types.rs b/creusot/tests/should_succeed/constrained_types.rs
index 9d51754f12..e73dc6309f 100644
--- a/creusot/tests/should_succeed/constrained_types.rs
+++ b/creusot/tests/should_succeed/constrained_types.rs
@@ -1,10 +1,10 @@
 extern crate creusot_contracts;
 
-use creusot_contracts::{logic::OrdLogic, *};
+use creusot_contracts::{logic::PartialOrdLogic, *};
 
 extern_spec! {
     impl<U: PartialOrd<U> + DeepModel, T: PartialOrd<T> + DeepModel> PartialOrd for (U, T)
-    where U::DeepModelTy: OrdLogic, T::DeepModelTy: OrdLogic
+    where U::DeepModelTy: PartialOrdLogic, T::DeepModelTy: PartialOrdLogic
     {
         #[ensures(result == self.deep_model().lt_log(o.deep_model()))]
         fn lt(&self, o: &(U, T)) -> bool;