diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index 1469bbbb42..30139349ab 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -309,7 +309,7 @@ infix `*`    := rat.mul
 prefix `-`   := rat.neg
 postfix `⁻¹` := rat.inv
 
-definition sub (a b : rat) : rat := a + (-b)
+definition sub [reducible] (a b : rat) : rat := a + (-b)
 
 infix `-`    := rat.sub
 
@@ -426,6 +426,7 @@ section migrate_algebra
 
   local attribute rat.discrete_field [instance]
   definition divide (a b : rat) := algebra.divide a b
+  infix `/` := divide
   definition dvd (a b : rat) := algebra.dvd a b
 
   migrate from algebra with rat
diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean
index 65a05d7b34..c07b0c1a3c 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -265,8 +265,15 @@ section migrate_algebra
   definition abs (n : rat) : rat := algebra.abs n
   definition sign (n : rat) : rat := algebra.sign n
 
+  definition max (a b : rat) : rat := algebra.max a b
+  definition min (a b : rat) : rat := algebra.min a b
+  --set_option migrate.trace true
   migrate from algebra with rat
     replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign, dvd → dvd,
-      divide → divide
+      divide → divide, max → max, min → min
+
+attribute le.trans lt.trans lt_of_lt_of_le lt_of_le_of_lt ge.trans gt.trans gt_of_gt_of_ge
+                   gt_of_ge_of_gt [trans]
+
 end migrate_algebra
 end rat