diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeFamilies     #-}
 {-# LANGUAGE TypeOperators, TypeSynonymInstances                       #-}
 module Proof.Equational ((:=:)(..), Equality(..), Preorder(..), reflexivity'
-                        ,(:\/:), (:/\:), (=>=), (=~=), Leibniz(..)
+                        ,(:\/:), (:/\:), (=<=), (=>=), (=~=), Leibniz(..)
                         , Reason(..), because, by, (===), start, byDefinition
                         , admitted, Proxy(..), cong, cong'
                         , Proposition(..), (:~>), FromBool (..)
@@ -83,15 +83,18 @@
 because = Because
 by      = Because
 
-infixl 4 ===, =>=, =~=
+infixl 4 ===, =<=, =~=, =>=
 infix 5 `Because`
 infix 5 `because`
 
-(=>=) :: Preorder r => r x y -> Reason r y z -> r x z
-eq =>= (_ `Because` eq') = transitivity eq eq'
+(=<=) :: Preorder r => r x y -> Reason r y z -> r x z
+eq =<= (_ `Because` eq') = transitivity eq eq'
 
+(=>=) :: Preorder r => r y z -> Reason r x y -> r x z
+eq =>= (_ `Because` eq') = transitivity eq' eq
+
 (===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
-(===) = (=>=)
+(===) = (=<=)
 
 (=~=) :: Preorder r => r x y -> Sing y -> r x y
 eq =~= _ = eq
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -2,7 +2,7 @@
 --  documentation, see http://haskell.org/cabal/users-guide/
 
 name:                equational-reasoning
-version:             0.0.3.0
+version:             0.0.4.0
 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds
 -- description:         
 license:             BSD3