diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,11 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v2.6.2 _(2024-09-04)_
+
+### Changed
+- Functions for enconding cardinality-constraints in `Language.Hasmtlib.Counting` now use specialized encodings for some cardinalities - improving solvers efficiency.
+
 ## v2.6.1 _(2024-09-02)_
 
 ### Added
diff --git a/hasmtlib.cabal b/hasmtlib.cabal
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               2.6.1
+version:               2.6.2
 synopsis:              A monad for interfacing with external SMT solvers
 description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
diff --git a/src/Language/Hasmtlib/Counting.hs b/src/Language/Hasmtlib/Counting.hs
--- a/src/Language/Hasmtlib/Counting.hs
+++ b/src/Language/Hasmtlib/Counting.hs
@@ -10,7 +10,9 @@
 
 Therefore additional information for the temporal summation may need to be provided.
 
-E.g. if your logic is \"QF_LIA\" you would want @count \@IntSort $ ...@
+E.g. if your logic is \"QF_LIA\" you would want @'count'' \@'IntSort' $ ...@
+
+It is worth noting that some cardinality constraints use optimized encodings, such as @'atLeast' 1 ≡ 'or'@.
 -}
 module Language.Hasmtlib.Counting
 (
@@ -31,6 +33,7 @@
 import Prelude hiding (not, (&&), (||), or)
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Expr
+import Language.Hasmtlib.Boolean
 import Data.Proxy
 
 -- | Wrapper for 'count' which takes a 'Proxy'.
@@ -43,17 +46,29 @@
 count = count' (Proxy @t)
 {-# INLINE count #-}
 
--- | Out of many bool-expressions build a formula which encodes that __at most__ 'k' of them are 'true'.
-atMost  :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
-atMost  k = (<=? k) . count
-{-# INLINEABLE atMost #-}
+-- | Out of many bool-expressions build a formula which encodes that __at most__ @k@ of them are 'true'.
+atMost  :: forall t f. (Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
+atMost (Constant 0) = nand
+atMost (Constant 1) = atMostOneLinear
+atMost k = (<=? k) . count
+{-# INLINE atMost #-}
 
--- | Out of many bool-expressions build a formula which encodes that __at least__ 'k' of them are 'true'.
-atLeast :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
+atMostOneLinear :: (Foldable f, Boolean b) => f b -> b
+atMostOneLinear xs =
+  let (_, sz) = foldr (plus . (, false)) (false, false) xs
+   in not sz
+  where
+    plus (xe, xz) (ye, yz) = (xe || ye, xz || yz || (xe && ye))
+
+-- | Out of many bool-expressions build a formula which encodes that __at least__ @k@ of them are 'true'.
+atLeast :: forall t f. (Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
+atLeast (Constant 0) = const true
+atLeast (Constant 1) = or
 atLeast k = (>=? k) . count
-{-# INLINEABLE atLeast #-}
+{-# INLINE atLeast #-}
 
--- | Out of many bool-expressions build a formula which encodes that __exactly__ 'k' of them are 'true'.
-exactly :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
+-- | Out of many bool-expressions build a formula which encodes that __exactly__ @k@ of them are 'true'.
+exactly :: forall t f. (Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
+exactly (Constant 0) = nand
 exactly k = (=== k) . count
-{-# INLINEABLE exactly #-}
+{-# INLINE exactly #-}
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -737,6 +737,9 @@
   xor x (Constant (BoolValue y)) = if y then not x else x
   xor x y = Xor x y
   {-# INLINE xor #-}
+  (Constant (BoolValue False)) ==> _ = true
+  x ==> y  = Impl x y
+  {-# INLINE (==>) #-}
   (<==>) = (===)
   {-# INLINE (<==>) #-}
 
diff --git a/src/Language/Hasmtlib/Type/Relation.hs b/src/Language/Hasmtlib/Type/Relation.hs
--- a/src/Language/Hasmtlib/Type/Relation.hs
+++ b/src/Language/Hasmtlib/Type/Relation.hs
@@ -203,7 +203,7 @@
 -- | Returns a list of 'Expr' 'BoolSort' indicating whether the projection on
 -- given element \( x \in A \) holds for every element in the codomain:
 --
--- \( \{ (x,y) \in R \mid y \in codomain(B) \} \)
+-- \( \{ (x,y) \in R \mid y \in codomain(R) \} \)
 image :: (Ix a, Ix b) => Relation a b -> a -> [Expr BoolSort]
 image r x = mapMaybe ((r !?) . (x,)) (codomain r)
 {-# INLINE image #-}
@@ -211,7 +211,7 @@
 -- | Returns a list of 'Expr' 'BoolSort' indicating whether the projection on
 -- given element \( y \in B \) holds for every element in the domain:
 --
--- \( \{ (x,y) \in R \mid x \in domain(A) \} \)
+-- \( \{ (x,y) \in R \mid x \in domain(R) \} \)
 preimage :: (Ix a, Ix b) => Relation a b -> b -> [Expr BoolSort]
 preimage r y = mapMaybe ((r !?) . (,y)) (domain r)
 {-# INLINE preimage #-}