From 681f431d4b08f2e1e5da840a8c39f4e759eccf64 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rlewis1@andrew.cmu.edu>
Date: Tue, 26 May 2015 11:52:34 +1000
Subject: [PATCH] feat(library/data/rat): make rat subtraction reducible, fix
 migration of min/max

---
 library/data/rat/basic.lean | 3 ++-
 library/data/rat/order.lean | 9 ++++++++-
 2 files changed, 10 insertions(+), 2 deletions(-)

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