diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,28 @@
+0.12 [2020.02.03]
+-----------------
+* Relax the type signature for `divideTimes`:
+
+  ```diff
+  -dividesTimes :: (Divides a b, Divides a c) :- Divides a (b * c)
+  +dividesTimes ::  Divides a b               :- Divides a (b * c)
+  ```
+
+* Simplify the type signature of `dividesDef`:
+
+  ```diff
+  -dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ b)
+  +dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)
+  ```
+
+  The original type of `diviesDef` can be (partially) recovered by defining
+  it in terms of the new `dividesDef`:
+
+  ```hs
+  dividesDef' :: forall a b. (1 <= a, Divides a b) :- ((a * Div b a) ~ b)
+  dividesDef' = Sub $ case (dividesDef @a @b, euclideanNat @a @b) of
+    (Sub Dict, Sub Dict) -> Dict
+  ```
+
 0.11.2 [2019.09.06]
 -------------------
 * Depend on the `type-equality` compatibility library so that `(:~~:)` may be
diff --git a/constraints.cabal b/constraints.cabal
--- a/constraints.cabal
+++ b/constraints.cabal
@@ -1,6 +1,6 @@
 name:          constraints
 category:      Constraints
-version:       0.11.2
+version:       0.12
 license:       BSD2
 cabal-version: >= 1.10
 license-file:  LICENSE
diff --git a/src/Data/Constraint.hs b/src/Data/Constraint.hs
--- a/src/Data/Constraint.hs
+++ b/src/Data/Constraint.hs
@@ -208,6 +208,7 @@
 infixr 9 :-
 infixr 9 ⊢
 
+-- | Type entailment, as written with a single character.
 type (⊢) = (:-)
 
 -- | This is the type of entailment.
diff --git a/src/Data/Constraint/Nat.hs b/src/Data/Constraint/Nat.hs
--- a/src/Data/Constraint/Nat.hs
+++ b/src/Data/Constraint/Nat.hs
@@ -323,7 +323,7 @@
 dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c)
 dividesPlus = Sub axiom
 
-dividesTimes :: (Divides a b, Divides a c) :- Divides a (b * c)
+dividesTimes :: Divides a b :- Divides a (b * c)
 dividesTimes = Sub axiom
 
 dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)
@@ -332,7 +332,10 @@
 dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c)
 dividesMax = Sub axiom
 
-dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ b)
+-- This `dividesDef` is simpler and more convenient than Divides a b :- ((a * Div b a) ~ b)
+-- because the latter can be easily derived via 'euclideanNat', but not vice versa.
+
+dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)
 dividesDef = Sub axiom
 
 dividesPow :: (1 <= n, Divides a b) :- Divides a (b^n)