diff --git a/Algebra/Algorithms/Groebner.hs b/Algebra/Algorithms/Groebner.hs
--- a/Algebra/Algorithms/Groebner.hs
+++ b/Algebra/Algorithms/Groebner.hs
@@ -9,7 +9,8 @@
                                    , buchberger, syzygyBuchberger, simpleBuchberger, primeTestBuchberger
                                    , reduceMinimalGroebnerBasis, minimizeGroebnerBasis
                                    -- * Ideal operations
-                                   , isIdealMember, intersection, thEliminationIdeal
+                                   , isIdealMember, intersection, thEliminationIdeal, thEliminationIdealWith
+                                   , unsafeThEliminationIdealWith
                                    , quotIdeal, quotByPrincipalIdeal
                                    , saturationIdeal, saturationByPrincipalIdeal
                                    ) where
@@ -24,6 +25,7 @@
 import           Data.Function
 import qualified Data.Heap               as H
 import           Data.List
+import           Data.Proxy
 import           Data.STRef
 import           Numeric.Algebra
 import           Prelude                 hiding (Num (..), recip)
@@ -165,25 +167,56 @@
              => OrderedPolynomial k order n -> [OrderedPolynomial k order n] -> Bool
 groebnerTest f fs = f `modPolynomial` fs == zero
 
--- | Calculate n-th elimination ideal.
+-- | Calculate n-th elimination ideal using 'Lex' ordering.
 thEliminationIdeal :: ( IsMonomialOrder ord, Field k, IsPolynomial k m, IsPolynomial k (m :-: n)
                       , (n :<<= m) ~ True)
                    => SNat n
                    -> Ideal (OrderedPolynomial k ord m)
-                   -> Ideal (OrderedPolynomial k Lex (m :-: n))
-thEliminationIdeal n ideal =
-    toIdeal $ [ transformMonomial (dropV n) f
-              | f <- calcGroebnerBasisWith Lex ideal
-              , all (all (== 0) . take (toInt n) . toList . snd) $ getTerms f
-              ]
+                   -> Ideal (OrderedPolynomial k ord (m :-: n))
+thEliminationIdeal n =
+    case singInstance n of
+      SingInstance ->
+        case weightVInstance n of
+          ToWeightVectorInstance -> mapIdeal (changeOrderProxy Proxy) . thEliminationIdealWith (weightedEliminationOrder n) n
 
+-- | Calculate n-th elimination ideal using the specified n-th elimination type order.
+thEliminationIdealWith :: ( IsMonomialOrder ord, Field k, IsPolynomial k m, IsPolynomial k (m :-: n)
+                      , (n :<<= m) ~ True, EliminationType n ord, IsMonomialOrder ord')
+                   => ord
+                   -> SNat n
+                   -> Ideal (OrderedPolynomial k ord' m)
+                   -> Ideal (OrderedPolynomial k ord (m :-: n))
+thEliminationIdealWith ord n ideal =
+    case singInstance n of
+      SingInstance ->  toIdeal $ [ transformMonomial (dropV n) f
+                                 | f <- calcGroebnerBasisWith ord ideal
+                                 , all (all (== 0) . take (toInt n) . toList . snd) $ getTerms f
+                                 ]
+
+-- | Calculate n-th elimination ideal using the specified n-th elimination type order.
+-- This function should be used carefully because it does not check whether the given ordering is
+-- n-th elimintion type or not.
+unsafeThEliminationIdealWith :: ( IsMonomialOrder ord, Field k, IsPolynomial k m, IsPolynomial k (m :-: n)
+                                , (n :<<= m) ~ True, IsMonomialOrder ord')
+                             => ord
+                             -> SNat n
+                             -> Ideal (OrderedPolynomial k ord' m)
+                             -> Ideal (OrderedPolynomial k ord (m :-: n))
+unsafeThEliminationIdealWith ord n ideal =
+    case singInstance n of
+      SingInstance ->  toIdeal $ [ transformMonomial (dropV n) f
+                                 | f <- calcGroebnerBasisWith ord ideal
+                                 , all (all (== 0) . take (toInt n) . toList . snd) $ getTerms f
+                                 ]
+
+
 -- | An intersection ideal of given ideals.
 intersection :: forall r k n ord.
                 ( IsMonomialOrder ord, Field r, IsPolynomial r k, IsPolynomial r n
                 , IsPolynomial r (k :+: n)
                 )
              => Vector (Ideal (OrderedPolynomial r ord n)) k
-             -> Ideal (OrderedPolynomial r Lex n)
+             -> Ideal (OrderedPolynomial r ord n)
 intersection Nil = Ideal $ singletonV one
 intersection idsv@(_ :- _) =
     let sk = sLengthV idsv
@@ -193,22 +226,22 @@
         j = foldr appendIdeal (principalIdeal (one - foldr (+) zero ts)) tis
     in case plusMinusEqR sn sk of
          Eql -> case propToBoolLeq (plusLeqL sk sn) of
-                  LeqTrueInstance -> sk `thEliminationIdeal` j
+                  LeqTrueInstance -> thEliminationIdeal sk j
 
 -- | Ideal quotient by a principal ideals.
 quotByPrincipalIdeal :: (Field k, IsPolynomial k n, IsMonomialOrder ord)
                      => Ideal (OrderedPolynomial k ord n)
                      -> OrderedPolynomial k ord n
-                     -> Ideal (OrderedPolynomial k Lex n)
+                     -> Ideal (OrderedPolynomial k ord n)
 quotByPrincipalIdeal i g =
     case intersection (i :- (Ideal $ singletonV g) :- Nil) of
-      Ideal gs -> Ideal $ mapV (snd . head . (`divPolynomial` [changeOrder Lex g])) gs
+      Ideal gs -> Ideal $ mapV (snd . head . (`divPolynomial` [g])) gs
 
 -- | Ideal quotient by the given ideal.
 quotIdeal :: forall k ord n. (IsPolynomial k n, Field k, IsMonomialOrder ord)
           => Ideal (OrderedPolynomial k ord n)
           -> Ideal (OrderedPolynomial k ord n)
-          -> Ideal (OrderedPolynomial k Lex n)
+          -> Ideal (OrderedPolynomial k ord n)
 quotIdeal i (Ideal g) =
   case singInstance (sLengthV g) of
     SingInstance ->
@@ -221,7 +254,7 @@
                            -> OrderedPolynomial k ord n -> Ideal (OrderedPolynomial k Lex n)
 saturationByPrincipalIdeal is g =
   case propToClassLeq $ leqSucc (sDegree g) of
-    LeqInstance -> sOne `thEliminationIdeal` addToIdeal (one - (castPolynomial g * var sOne)) (mapIdeal (shiftR sOne) is)
+    LeqInstance -> thEliminationIdealWith Lex sOne $ addToIdeal (one - (castPolynomial g * var sOne)) (mapIdeal (shiftR sOne) is)
 
 -- | Saturation ideal
 saturationIdeal :: forall k ord n. (IsPolynomial k n, Field k, IsMonomialOrder ord)
diff --git a/Algebra/Algorithms/Groebner/Monomorphic.hs b/Algebra/Algorithms/Groebner/Monomorphic.hs
--- a/Algebra/Algorithms/Groebner/Monomorphic.hs
+++ b/Algebra/Algorithms/Groebner/Monomorphic.hs
@@ -13,7 +13,7 @@
     , primeTestBuchberger, primeTestBuchbergerWith
     , simpleBuchberger, simpleBuchbergerWith
     -- * Ideal operations
-    , isIdealMember, intersection, thEliminationIdeal, eliminate
+    , isIdealMember, intersection, thEliminationIdeal, eliminate, thEliminationIdealWith, eliminateWith
     , quotIdeal, quotByPrincipalIdeal
     , saturationIdeal, saturationByPrincipalIdeal
     -- * Re-exports
@@ -187,8 +187,9 @@
     _ -> error "impossible happend!"
 
 -- | Computes the ideal with specified variables eliminated.
-eliminate :: forall r. Groebnerable r => [Variable] -> [Polynomial r] -> [Polynomial r]
-eliminate elvs j =
+eliminateWith :: forall r ord . (IsMonomialOrder ord, Groebnerable r)
+              => ord -> [Variable] -> [Polynomial r] -> [Polynomial r]
+eliminateWith ord elvs j =
   case promoteListWithVarOrder (els ++ rest) j :: Monomorphic ([] :.: Poly.OrderedPolynomial r Poly.Lex) of
     Monomorphic (Comp fs) ->
       case promote k of
@@ -206,14 +207,20 @@
                               LeqTrueInstance ->
                                 case singInstance (newDim %- sk) of
                                   SingInstance ->
-                                    map (renameVars rest) $ demoteComposed $ sk `Gr.thEliminationIdeal` toIdeal fs'
+                                    map (renameVars rest) $ demoteComposed $ Gr.unsafeThEliminationIdealWith ord sk (toIdeal fs')
   where
     vars = nub $ sort $ concatMap buildVarsList j
     (els, rest) = partition (`elem` elvs) vars
     k = length els
 
+eliminate :: forall r.  Groebnerable r => [Variable] -> [Polynomial r] -> [Polynomial r]
+eliminate = eliminateWith Lex
+
 -- | Computes nth elimination ideal.
 thEliminationIdeal :: Groebnerable r => Int -> [Polynomial r] -> [Polynomial r]
-thEliminationIdeal k j = eliminate (take k vars) j
+thEliminationIdeal = thEliminationIdealWith Lex
+
+thEliminationIdealWith :: (IsMonomialOrder ord, Groebnerable r) => ord -> Int -> [Polynomial r] -> [Polynomial r]
+thEliminationIdealWith ord k j = eliminateWith ord (take k vars) j
   where
     vars = nub $ sort $ concatMap buildVarsList j
diff --git a/Algebra/Internal.hs b/Algebra/Internal.hs
--- a/Algebra/Internal.hs
+++ b/Algebra/Internal.hs
@@ -10,7 +10,7 @@
                         , SZero, SOne, STwo, SThree
                         , lengthV, sLengthV, takeV, dropV, splitAtV, appendV
                         , foldrV, foldlV, singletonV, zipWithV, toList, allV
-                        , mapV, headV, tailV
+                        , mapV, headV, tailV, splitAtLess
                         , Leq(..), (:<<=), (:<=), LeqInstance(..)
                         , LeqTrueInstance(..), boolToPropLeq, boolToClassLeq
                         , propToClassLeq, propToBoolLeq
@@ -219,6 +219,14 @@
 takeV :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a n
 takeV n = fst . splitAtV n
 
+splitAtLess :: SNat n -> Vector a m -> (Vector a (Min n m), Vector a (m :-: n))
+splitAtLess SZ v = case zAbsorbsMinL (sLengthV v) of
+                     Eql -> (Nil, v)
+splitAtLess (SS _) Nil = (Nil, Nil)
+splitAtLess (SS n) (x :- xs) =
+  case splitAtLess n xs of
+    (ys, zs) -> (x :- ys, zs)
+
 toInt :: SNat n -> Int
 toInt SZ     = 0
 toInt (SS n) = 1 + toInt n
@@ -382,7 +390,7 @@
     LeqTrueInstance -> eqlTrans (eqSuccMinus (n %+ m) m) (eqPreservesS $ plusMinusEqL n m)
 
 plusMinusEqR :: SNat n -> SNat m -> Eql ((m :+: n) :-: m) n
-plusMinusEqR n m = eqlTrans (minusCongEq (plusCommutative n m) m) (plusMinusEqL n m)
+plusMinusEqR n m = eqlTrans (minusCongEq (plusCommutative m n) m) (plusMinusEqL n m)
 
 data LeqTrueInstance a b where
   LeqTrueInstance :: (a :<<= b) ~ True => LeqTrueInstance a b
diff --git a/Algebra/Ring/Noetherian.hs b/Algebra/Ring/Noetherian.hs
--- a/Algebra/Ring/Noetherian.hs
+++ b/Algebra/Ring/Noetherian.hs
@@ -10,6 +10,7 @@
 import           Data.Ord
 import           Data.Ratio
 import           Numeric.Algebra
+import qualified Numeric.Algebra         as NA
 import qualified Numeric.Algebra.Complex as NA
 import           Prelude                 hiding (negate, subtract, (*), (+),
                                           (-))
@@ -24,6 +25,18 @@
 instance (Commutative (NA.Complex r), Ring (NA.Complex r)) => NoetherianRing (NA.Complex r) where
 instance (Commutative (C.Complex r), Ring (C.Complex r)) => NoetherianRing (C.Complex r) where
 instance Integral n => NoetherianRing (Ratio n)
+
+instance Integral n => InvolutiveMultiplication (Ratio n) where
+  adjoint = id
+instance Integral n => InvolutiveSemiring (Ratio n)
+
+instance Integral n => TriviallyInvolutive (Ratio n)
+
+instance (P.Num n) => P.Num (NA.Complex n) where
+  fromInteger n = NA.Complex (P.fromInteger n) 0
+  negate (NA.Complex x y) = NA.Complex (P.negate x) (P.negate y)
+  NA.Complex x y + NA.Complex z w = NA.Complex (x P.+ y) (z P.+ w)
+  NA.Complex x y * NA.Complex z w = NA.Complex (x P.* z P.- y P.* w) (x P.* w P.+ y P.* z)
 
 instance Division (Ratio Integer) where
   recip = P.recip
diff --git a/Algebra/Ring/Polynomial.hs b/Algebra/Ring/Polynomial.hs
--- a/Algebra/Ring/Polynomial.hs
+++ b/Algebra/Ring/Polynomial.hs
@@ -1,20 +1,23 @@
 {-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances #-}
 {-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, MultiParamTypeClasses        #-}
-{-# LANGUAGE PolyKinds, ScopedTypeVariables, StandaloneDeriving              #-}
-{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances, ViewPatterns #-}
+{-# LANGUAGE OverlappingInstances, PolyKinds, ScopedTypeVariables            #-}
+{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators                 #-}
+{-# LANGUAGE UndecidableInstances, ViewPatterns                              #-}
 {-# OPTIONS_GHC -fno-warn-orphans -fno-warn-type-defaults                    #-}
 module Algebra.Ring.Polynomial
-    ( Polynomial, Monomial, MonomialOrder, Order
-    , lex, revlex, graded, grlex, grevlex, transformMonomial
+    ( Polynomial, Monomial, MonomialOrder, EliminationType, EliminationOrder
+    , WeightedEliminationOrder, eliminationOrder, weightedEliminationOrder
+    , lex, revlex, graded, grlex, grevlex, productOrder, productOrder'
+    , transformMonomial, WeightProxy(..), weightOrder
     , IsPolynomial, coeff, lcmMonomial, sPolynomial, polynomial
-    , castMonomial, castPolynomial, toPolynomial, changeOrder
-    , scastMonomial, scastPolynomial, OrderedPolynomial, showPolynomialWithVars
+    , castMonomial, castPolynomial, toPolynomial, changeOrder, changeOrderProxy
+    , scastMonomial, scastPolynomial, OrderedPolynomial, showPolynomialWithVars, showPolynomialWith, showRational, ToWeightVectorInstance(..), weightVInstance
     , normalize, injectCoeff, varX, var, getTerms, shiftR, orderedBy
     , divs, tryDiv, fromList -- , genVarsV
     , leadingTerm, leadingMonomial, leadingCoeff, genVars, sDegree
     , OrderedMonomial(..), Grevlex(..), Revlex(..), Lex(..), Grlex(..)
-    , IsOrder, IsMonomialOrder)  where
-
+    , ProductOrder (..), WeightOrder(..)
+    , IsOrder(..), IsMonomialOrder)  where
 import           Algebra.Internal
 import           Algebra.Ring.Noetherian
 import           Control.Arrow
@@ -26,7 +29,8 @@
 import           Data.Monoid
 import           Data.Ord
 import           Data.Proxy
-import           Numeric.Algebra
+import           Data.Ratio
+import           Numeric.Algebra         hiding (Order(..))
 import           Prelude                 hiding (lex, (*), (+), (-), (^), (^^), recip, negate)
 import qualified Prelude                 as P
 
@@ -94,6 +98,53 @@
 data Revlex = Revlex            -- Reversed lexicographical order
               deriving (Show, Eq, Ord)
 
+data ProductOrder n a b where
+  ProductOrder :: SNat n -> ord -> ord' -> ProductOrder n ord ord'
+
+productOrder :: forall ord ord' n m. (IsOrder ord, IsOrder ord', Sing n)
+             => Proxy (ProductOrder n ord ord') -> Monomial m -> Monomial m -> Ordering
+productOrder _ m m' =
+  case sing :: SNat n of
+    n -> case (splitAtLess n m, splitAtLess n m') of
+           ((xs, xs'), (ys, ys')) -> cmpMonomial (Proxy :: Proxy ord) xs ys <> cmpMonomial (Proxy :: Proxy ord') xs' ys'
+
+productOrder' :: forall n ord ord' m.(IsOrder ord, IsOrder ord')
+              => SNat n -> ord -> ord' -> Monomial m -> Monomial m -> Ordering
+productOrder' n ord ord' =
+  case singInstance n of SingInstance -> productOrder (toProxy $ ProductOrder n ord ord')
+
+-- | Data.Proxy provides kind-polymorphic 'Proxy' data-type, but due to bug of GHC 7.4.1,
+-- It canot be used as kind-polymorphic. So I define another type here.
+data WeightProxy (v :: [Nat]) where
+  NilWeight  :: WeightProxy '[]
+  ConsWeight :: SNat n -> WeightProxy v -> WeightProxy (n ': v)
+
+data WeightOrder (v :: [Nat]) (ord :: *) where
+  WeightOrder :: WeightProxy (v :: [Nat]) -> ord -> WeightOrder v ord
+
+data Proxy' (vs :: [Nat]) = Proxy'
+
+class ToWeightVector (vs :: [Nat]) where
+  toWeightV :: Proxy' vs -> [Int]
+
+instance ToWeightVector '[] where
+  toWeightV Proxy' = []
+
+instance (Sing n, ToWeightVector ns) => ToWeightVector (n ': ns) where
+  toWeightV Proxy' = toInt (sing :: SNat n) : toWeightV (Proxy' :: Proxy' ns)
+
+weightOrder :: forall ns ord m. (ToWeightVector ns, IsOrder ord)
+            => Proxy (WeightOrder ns ord) -> Monomial m -> Monomial m -> Ordering
+weightOrder Proxy m m' = comparing toW m m' <> cmpMonomial (Proxy :: Proxy ord) m m'
+  where
+    toW = zipWith (*) (toWeightV (Proxy' :: Proxy' ns)) . toList
+
+instance (ToWeightVector ws, IsOrder ord) => IsOrder (WeightOrder ws ord) where
+  cmpMonomial p = weightOrder p
+
+instance (IsOrder ord, IsOrder ord', Sing n) => IsOrder (ProductOrder n ord ord') where
+  cmpMonomial p = productOrder p
+
 -- They're all total orderings.
 instance IsOrder Grevlex where
   cmpMonomial _ = grevlex
@@ -115,7 +166,47 @@
 instance IsMonomialOrder Grlex
 instance IsMonomialOrder Grevlex
 instance IsMonomialOrder Lex
+instance (Sing n, IsMonomialOrder o, IsMonomialOrder o') => IsMonomialOrder (ProductOrder n o o')
+instance (ToWeightVector ws, IsMonomialOrder ord) => IsMonomialOrder (WeightOrder ws ord)
 
+-- | Monomial order which can be use to calculate n-th elimination ideal.
+-- This should judge it as bigger that contains variables to eliminate.
+class (IsMonomialOrder ord, Sing n) => EliminationType n ord
+instance Sing n => EliminationType n Lex
+instance (Sing n, IsMonomialOrder ord, IsMonomialOrder ord') => EliminationType n (ProductOrder n ord ord')
+instance (IsMonomialOrder ord) => EliminationType Z (WeightOrder '[] ord)
+instance (IsMonomialOrder ord, ToWeightVector ns, EliminationType n (WeightOrder ns ord))
+    => EliminationType (S n) (WeightOrder (One ': ns) ord)
+
+type EliminationOrder n = ProductOrder n Grevlex Grevlex
+
+data ToWeightVectorInstance n where
+  ToWeightVectorInstance :: (EliminationType n (WeightedEliminationOrder n), ToWeightVector (EWeight n)) => ToWeightVectorInstance n
+
+weightVInstance :: SNat n -> ToWeightVectorInstance n
+weightVInstance SZ = ToWeightVectorInstance
+weightVInstance (SS n) =
+  case weightVInstance n of
+    ToWeightVectorInstance -> ToWeightVectorInstance
+
+eliminationOrder :: SNat n -> EliminationOrder n
+eliminationOrder n =
+  case singInstance n of
+    SingInstance -> ProductOrder n Grevlex Grevlex
+
+weightedEliminationOrder :: SNat n -> WeightedEliminationOrder n
+weightedEliminationOrder n = WeightOrder (mkWeight n) Grevlex
+
+mkWeight :: SNat n -> WeightProxy (EWeight n)
+mkWeight SZ     = NilWeight
+mkWeight (SS n) = ConsWeight sOne $ mkWeight n
+
+type family EWeight n :: [Nat]
+type instance EWeight Z = '[]
+type instance EWeight (S n) = One ': EWeight n
+
+type WeightedEliminationOrder n = WeightOrder (EWeight n) Grevlex
+
 -- | Special ordering for ordered-monomials.
 instance (Eq (Monomial n), IsOrder name) => Ord (OrderedMonomial name n) where
   OrderedMonomial m `compare` OrderedMonomial n = cmpMonomial (Proxy :: Proxy name) m n
@@ -171,7 +262,7 @@
 instance (IsOrder order, IsPolynomial r n) => Group (OrderedPolynomial r order n) where
   negate (Polynomial dic) = Polynomial $ fmap negate dic
 instance (IsOrder order, IsPolynomial r n) => LeftModule Integer (OrderedPolynomial r order n) where
-  n .* Polynomial dic = Polynomial $ fmap (n .*) dic  
+  n .* Polynomial dic = Polynomial $ fmap (n .*) dic
 instance (IsOrder order, IsPolynomial r n) => RightModule Integer (OrderedPolynomial r order n) where
   (*.) = flip (.*)
 instance (IsOrder order, IsPolynomial r n) => Additive (OrderedPolynomial r order n) where
@@ -195,6 +286,9 @@
 instance (Eq r, IsPolynomial r n, IsOrder order, Show r) => Show (OrderedPolynomial r order n) where
   show = showPolynomialWithVars [(n, "X_"++ show n) | n <- [1..]]
 
+instance (Sing n, IsOrder order) => Show (OrderedPolynomial Rational order n) where
+  show = showPolynomialWith [(n, "X_"++ show n) | n <- [1..]] showRational
+
 showPolynomialWithVars :: (Eq a, Show a, Sing n, NoetherianRing a, IsOrder ordering)
                        => [(Int, String)] -> OrderedPolynomial a ordering n -> String
 showPolynomialWithVars dic p0@(Polynomial d)
@@ -215,6 +309,44 @@
                      | otherwise = Just $ showVar n ++ "^" ++ show p
       showVar n = fromMaybe ("X_" ++ show n) $ lookup n dic
 
+data Coefficient = Zero | Negative String | Positive String | Eps
+                 deriving (Show, Eq, Ord)
+
+showRational :: (Integral a, Show a) => Ratio a -> Coefficient
+showRational r | r == 0    = Zero
+               | r >  0    = Positive $ formatRat r
+               | otherwise = Negative $ formatRat $ abs r
+  where
+    formatRat q | denominator q == 1 = show $ numerator q
+                | otherwise          = show (numerator q) ++ "/" ++ show (denominator q) ++ " "
+
+showPolynomialWith  :: (Eq a, Show a, Sing n, NoetherianRing a, IsOrder ordering)
+                    => [(Int, String)] -> (a -> Coefficient) -> OrderedPolynomial a ordering n -> String
+showPolynomialWith vDic showCoeff p0@(Polynomial d)
+    | p0 == zero = "0"
+    | otherwise  = catTerms $ mapMaybe procTerm $ M.toDescList d
+    where
+      catTerms [] = "0"
+      catTerms (x:xs) = concat $ showTerm True x : map (showTerm False) xs
+      showTerm isLeading (Zero, _) = if isLeading then "0" else ""
+      showTerm isLeading (Positive s, deg) = if isLeading then s ++ deg else " + " ++ s ++ deg
+      showTerm isLeading (Negative s, deg) = if isLeading then '-' : s ++ deg else " - " ++ s ++ deg
+      showTerm isLeading (Eps, deg) = if isLeading then deg else " + " ++ deg
+      procTerm (getMonomial -> deg, c)
+          | c == zero = Nothing
+          | otherwise =
+              let cKind = showCoeff c
+                  cff | isConstantMonomial deg && c == one        = Positive "1"
+                      | isConstantMonomial deg && c == negate one = Negative "1"
+                      | c == one = Positive ""
+                      | c == negate one = Negative ""
+                      | otherwise                                 = cKind
+              in Just $ (cff, unwords (mapMaybe showDeg (zip [1..] $ toList deg)))
+      showDeg (n, p) | p == 0    = Nothing
+                     | p == 1    = Just $ showVar n
+                     | otherwise = Just $ showVar n ++ "^" ++ show p
+      showVar n = fromMaybe ("X_" ++ show n) $ lookup n vDic
+
 isConstantMonomial :: (Eq a, Num a) => Vector a n -> Bool
 isConstantMonomial v = all (== 0) $ toList v
 
@@ -278,6 +410,10 @@
 changeOrder :: (Eq (Monomial n), IsOrder o, IsOrder o',  Sing n)
             => o' -> OrderedPolynomial k o n -> OrderedPolynomial k o' n
 changeOrder _ = unwrapped %~ M.mapKeys (OrderedMonomial . getMonomial)
+
+changeOrderProxy :: (Eq (Monomial n), IsOrder o, IsOrder o',  Sing n)
+            => Proxy o' -> OrderedPolynomial k o n -> OrderedPolynomial k o' n
+changeOrderProxy _ = unwrapped %~ M.mapKeys (OrderedMonomial . getMonomial)
 
 getTerms :: OrderedPolynomial k order n -> [(k, Monomial n)]
 getTerms = map (snd &&& getMonomial . fst) . M.toDescList . terms
diff --git a/Algebra/Ring/Polynomial/Monomorphic.hs b/Algebra/Ring/Polynomial/Monomorphic.hs
--- a/Algebra/Ring/Polynomial/Monomorphic.hs
+++ b/Algebra/Ring/Polynomial/Monomorphic.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs           #-}
 {-# LANGUAGE MultiParamTypeClasses, PolyKinds, RecordWildCards, TypeFamilies #-}
-{-# LANGUAGE TypeOperators, ViewPatterns                                     #-}
+{-# LANGUAGE TypeOperators, ViewPatterns, OverlappingInstances               #-}
 {-# OPTIONS_GHC -fno-warn-orphans                             #-}
 module Algebra.Ring.Polynomial.Monomorphic where
 import           Algebra.Internal
@@ -11,6 +11,7 @@
 import qualified Data.Map                as M
 import           Data.Maybe
 import qualified Numeric.Algebra         as NA
+import           Data.Ratio
 
 data Variable = Variable { varName  :: Char
                          , varIndex :: Maybe Int
@@ -96,8 +97,11 @@
 
 data PolynomialSetting r = PolySetting { dimension :: Monomorphic SNat
                                        , polyn     :: Polynomial r
-                                       } deriving (Show)
+                                       }
 
+instance (Integral a, Show a) => Show (Polynomial (Ratio a)) where
+  show = showRatPolynomial
+
 instance (Eq r, NoetherianRing r, Show r) => Show (Polynomial r) where
   show = showPolynomial
 
@@ -183,6 +187,15 @@
     Monomorphic f' ->
         case singInstance (Poly.sDegree f') of
           SingInstance -> Poly.showPolynomialWithVars dic f'
+  where
+    dic = zip [1..] $ map show $ buildVarsList f
+
+showRatPolynomial :: (Integral a, Show a) => Polynomial (Ratio a) -> String
+showRatPolynomial f =
+  case encodePolynomial f of
+    Monomorphic f' ->
+        case singInstance (Poly.sDegree f') of
+          SingInstance -> Poly.showPolynomialWith dic Poly.showRational f'
   where
     dic = zip [1..] $ map show $ buildVarsList f
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -19,6 +19,7 @@
 * Compute Groebner basis using Buchberger Algorithm
 * Ideal membership problem
 * Elimination ideal calculation
+    * This library provides the monomial orders of l-th elimination type other than lex order, such as elimination order, product order,...
 * Ideal operations
 	* Saturation Ideal, Quotient ideal,...
 
diff --git a/computational-algebra.cabal b/computational-algebra.cabal
--- a/computational-algebra.cabal
+++ b/computational-algebra.cabal
@@ -2,7 +2,7 @@
 -- further documentation, see http://haskell.org/cabal/users-guide/
 
 name:                computational-algebra
-version:             0.1.1.0
+version:             0.1.2.0
 synopsis:            Well-kinded computational algebra library, currently supporting Groebner basis.
 description:         Dependently-typed computational algebra libray for Groebner basis.
 homepage:            https://github.com/konn/computational-algebra
diff --git a/examples/monomorphic.hs b/examples/monomorphic.hs
--- a/examples/monomorphic.hs
+++ b/examples/monomorphic.hs
@@ -40,7 +40,7 @@
 main :: IO ()
 main = do
   putStrLn $ unwords ["(" ++ show (x + 1) ++ ")^2", "="
-                     , show $ (x + 1) ^^2 ]
+                     , show $ show $ (x + 1) ^^2 ]
   putStrLn $ unwords ["(" ++ show (x + 1) ++ ")(" ++ show (x - 1) ++ ")", "="
                      , show $ (x + 1) * (x - 1) ]
   putStrLn $ unwords ["(" ++ show (x - 1) ++ ")(" ++ show (y^^2 + y - 1) ++ ")", "="
@@ -59,7 +59,7 @@
   putStrLn "Using elimination ideal, this can be automatically solved."
   putStrLn "We calculate this with theory of Groebner basis with respect to 'lex'."
   putStrLn "This might take a while. please wait..."
-  print heron
+  putStrLn $ show heron
   putStrLn "In equation above, X_1, X_2, X_3 and X_4 stands for a, b, c and S, respectively."
   putStrLn "The ideal has just one polynomial `f' as its only generator."
   putStrLn "Solving the equation `f = 0' assuming S > 0, we can get Heron's formula."
@@ -79,6 +79,7 @@
   let ex = parsePolyn src
   case (ls, ex) of
     ([], Right f)
-        | f `isIdealMember` rs -> putStrLn $ concat ["[YES!] ", show f, " ∈ 〈", intercalate ", " $ map show rs]
-        | otherwise            -> putStrLn $ concat ["[NO!] ", show f, " ∉ 〈", intercalate ", " $ map show rs]
+        | f `isIdealMember` rs -> putStrLn $ concat ["[YES!] ", show f, " ∈ 〈", intercalate ", " $ map show rs, "〉"]
+        | otherwise            ->
+            putStrLn $ concat ["[NO!] ", showRatPolynomial f, " ∉ 〈", intercalate ", " $ map show rs, "〉"]
     _ -> putStrLn "Parse error! try again." >> idealMembershipDemo
diff --git a/examples/polymorphic.hs b/examples/polymorphic.hs
--- a/examples/polymorphic.hs
+++ b/examples/polymorphic.hs
@@ -25,14 +25,17 @@
 type LexPolynomial r n = OrderedPolynomial r Lex n
 
 heron :: Ideal (LexPolynomial (Ratio Integer) (Two :+: Two))
-heron = sTwo `thEliminationIdeal` ideal
+heron = sTwo `thEliminationIdeal` heronIdeal
+
+heronIdeal :: Ideal (Polynomial (Ratio Integer) (Three :+: Three))
+heronIdeal = toIdeal [ 2 * s - a * y
+                     , b^^2 - (x^^2 + y^^2)
+                     , c^^2 - ( (a-x) ^^ 2 + y^^2)
+                     ]
   where
-    [x, y, a, b, c, s] = genVars (sThree %+ sThree) :: [LexPolynomial (Ratio Integer) (Three :+: Three)]
-    ideal = toIdeal [ 2 * s - a * y
-                    , b^^2 - (x^^2 + y^^2)
-                    , c^^2 - ( (a-x) ^^ 2 + y^^2)
-                    ]
+    [x, y, a, b, c, s] = genVars (sThree %+ sThree)
 
+
 main :: IO ()
 main = do
   putStrLn $ unwords ["(" ++ show (x + 1) ++ ")^2", "="
@@ -52,8 +55,15 @@
   putStrLn "Using elimination ideal, this can be automatically solved."
   putStrLn "We calculate this with theory of Groebner basis with respect to 'lex'."
   putStrLn "This might take a while. please wait..."
-  print heron
+  print $ sTwo `thEliminationIdeal` heronIdeal
   putStrLn "In equation above, X_1, X_2, X_3 and X_4 stands for a, b, c and S, respectively."
   putStrLn "The ideal has just one polynomial `f' as its only generator."
   putStrLn "Solving the equation `f = 0' assuming S > 0, we can get Heron's formula."
+  putStrLn ""
+  putStrLn "Let's use nother elimination type. We choose Grevlex × Grevlex: "
+  print $ thEliminationIdealWith (eliminationOrder sTwo) sTwo heronIdeal
+  putStrLn "And weighted order:"
+  print $ thEliminationIdealWith (weightedEliminationOrder sTwo) sTwo heronIdeal
+
+
 
diff --git a/examples/sandpit.hs b/examples/sandpit.hs
new file mode 100644
--- /dev/null
+++ b/examples/sandpit.hs
@@ -0,0 +1,42 @@
+module Main (module Algebra.Algorithms.Groebner.Monomorphic, module Algebra.Ring.Polynomial
+            , module Algebra.Ring.Polynomial.Parser, module Algebra.Ring.Polynomial.Monomorphic
+            , module Data.Ratio, module Main, module Algebra.Internal) where
+import           Algebra.Algorithms.Groebner.Monomorphic
+import           Algebra.Ring.Polynomial                 (Grevlex (..),
+                                                          Grlex (..), Lex (..),
+                                                          ProductOrder (..),
+                                                          WeightOrder (..),
+                                                          WeightProxy (..),
+                                                          eliminationOrder,
+                                                          weightedEliminationOrder)
+import           Algebra.Ring.Polynomial.Monomorphic
+import           Algebra.Ring.Polynomial.Parser
+import           Data.Ratio
+import Algebra.Internal
+import qualified Numeric.Algebra                         as NA
+
+var_x, var_y, var_z, var_t, var_u :: Variable
+[var_x, var_y, var_z, var_t, var_u] = map (flip Variable Nothing) "xyztu"
+
+x, y, z, t, u :: Polynomial Rational
+[x, y, z, t, u] = map injectVar [var_x, var_y, var_z, var_t, var_u]
+
+(.+), (.*), (.-) :: Polynomial Rational -> Polynomial Rational -> Polynomial Rational
+(.+) = (NA.+)
+(.*) = (NA.*)
+(.-) = (NA.-)
+
+infixl 6 .+, .-
+infixl 7 .*
+
+(^^^) :: Polynomial Rational -> NA.Natural -> Polynomial Rational
+(^^^) = NA.pow
+
+fromRight :: Either t t1 -> t1
+fromRight (Right a) = a
+
+parse :: String -> Polynomial Rational
+parse = fromRight . parsePolyn
+
+main :: IO ()
+main = return ()