diff --git a/library/data/pnat.lean b/library/data/pnat.lean
index 4a328329d..dcb6a7067 100644
--- a/library/data/pnat.lean
+++ b/library/data/pnat.lean
@@ -11,9 +11,11 @@ are those needed for that construction.
 import data.rat.order data.nat
 open nat rat subtype eq.ops
 
+definition pnat := { n : ℕ | n > 0 }
+
 namespace pnat
 
-definition pnat := { n : ℕ | n > 0 }
+protected definition prio := num.pred nat.prio
 
 notation `ℕ+` := pnat
 
@@ -35,19 +37,19 @@ protected definition le (p q : ℕ+) := p~ ≤ q~
 
 protected definition lt (p q : ℕ+) := p~ < q~
 
-definition pnat_has_add [instance] : has_add pnat :=
+definition pnat_has_add [instance] [priority pnat.prio] : has_add pnat :=
 has_add.mk pnat.add
 
-definition pnat_has_mul [instance] : has_mul pnat :=
+definition pnat_has_mul [instance] [priority pnat.prio] : has_mul pnat :=
 has_mul.mk pnat.mul
 
-definition pnat_has_le [instance] : has_le pnat :=
+definition pnat_has_le [instance] [priority pnat.prio] : has_le pnat :=
 has_le.mk pnat.le
 
-definition pnat_has_lt [instance] : has_lt pnat :=
+definition pnat_has_lt [instance] [priority pnat.prio] : has_lt pnat :=
 has_lt.mk pnat.lt
 
-definition pnat_has_one [instance] : has_one pnat :=
+definition pnat_has_one [instance] [priority pnat.prio] : has_one pnat :=
 has_one.mk (pos (1:nat) dec_trivial)
 
 protected lemma mul_def (p q : ℕ+) : p * q = tag (p~ * q~) (mul_pos (pnat_pos p) (pnat_pos q)) :=
@@ -62,44 +64,44 @@ rfl
 protected theorem pnat.eq {p q : ℕ+} : p~ = q~ → p = q :=
 subtype.eq
 
-definition pnat_le_decidable [instance] (p q : ℕ+) : decidable (p ≤ q) :=
-begin rewrite pnat.le_def, exact nat.decidable_le p~ q~ end
+protected definition decidable_lt : decidable_rel pnat.lt :=
+λa b, nat.decidable_lt a~ b~
 
-definition pnat_lt_decidable [instance] {p q : ℕ+} : decidable (p < q) :=
-begin rewrite pnat.lt_def, exact nat.decidable_lt p~ q~ end
+protected theorem le_refl (a : ℕ+) : a ≤ a :=
+begin rewrite pnat.le_def end
 
 protected theorem le_trans {p q r : ℕ+} : p ≤ q → q ≤ r → p ≤ r :=
 begin rewrite *pnat.le_def, apply nat.le_trans end
 
-definition max (p q : ℕ+) : ℕ+ :=
-tag (max p~ q~) (lt_of_lt_of_le (!pnat_pos) (!le_max_right))
+protected theorem le_antisymm {n m : ℕ+} : n ≤ m → m ≤ n → n = m :=
+begin rewrite +pnat.le_def, intros, apply (pnat.eq (nat.le_antisymm a a_1)) end
 
-protected theorem max_right (a b : ℕ+) : max a b ≥ b :=
-begin change b ≤ max a b, rewrite pnat.le_def, apply le_max_right end
+protected theorem le_iff_lt_or_eq (m n : ℕ+) : m ≤ n ↔ m < n ∨ m = n :=
+begin
+  rewrite [pnat.lt_def, pnat.le_def], apply iff.intro,
+  { intro, apply or.elim (nat.lt_or_eq_of_le a),
+    intro, apply or.intro_left, assumption,
+    intro, apply or.intro_right, apply pnat.eq, assumption },
+  { intro, apply or.elim a, apply nat.le_of_lt, intro, rewrite a_1 }
+end
 
-protected theorem max_left (a b : ℕ+) : max a b ≥ a :=
-begin change a ≤ max a b, rewrite pnat.le_def, apply le_max_left end
+protected theorem le_total (m n : ℕ+) : m ≤ n ∨ n ≤ m :=
+begin rewrite pnat.le_def, apply nat.le_total end
 
-protected theorem max_eq_right {a b : ℕ+} (H : a < b) : max a b = b :=
-begin rewrite pnat.lt_def at H, exact pnat.eq (max_eq_right_of_lt H) end
+protected theorem lt_irrefl (a : ℕ+) : ¬ a < a :=
+begin rewrite pnat.lt_def, apply nat.lt_irrefl end
 
-protected theorem max_eq_left {a b : ℕ+} (H : ¬ a < b) : max a b = a :=
-begin rewrite pnat.lt_def at H, exact pnat.eq (max_eq_left (le_of_not_gt H)) end
-
-protected theorem le_of_lt {a b : ℕ+} : a < b → a ≤ b :=
-begin rewrite [pnat.lt_def, pnat.le_def], apply nat.le_of_lt end
-
-protected theorem not_lt_of_ge {a b : ℕ+} : a ≤ b → ¬ (b < a) :=
-begin rewrite [pnat.lt_def, pnat.le_def], apply not_lt_of_ge end
-
-protected theorem le_of_not_gt {a b : ℕ+} : ¬ a < b → b ≤ a :=
-begin rewrite [pnat.lt_def, pnat.le_def], apply le_of_not_gt end
-
-protected theorem eq_of_le_of_ge {a b : ℕ+} : a ≤ b → b ≤ a → a = b :=
-begin rewrite [+pnat.le_def], intros H1 H2, exact pnat.eq (eq_of_le_of_ge H1 H2) end
-
-protected theorem le_refl (a : ℕ+) : a ≤ a :=
-begin rewrite pnat.le_def end
+protected definition decidable_linear_order [trans_instance] : decidable_linear_order pnat :=
+⦃ decidable_linear_order,
+  le              := pnat.le,
+  le_refl         := by apply pnat.le_refl,
+  le_trans        := by apply @pnat.le_trans,
+  le_antisymm     := by apply @pnat.le_antisymm,
+  lt              := pnat.lt,
+  lt_irrefl       := by apply pnat.lt_irrefl,
+  le_iff_lt_or_eq := by apply pnat.le_iff_lt_or_eq,
+  decidable_lt    := pnat.decidable_lt,
+  le_total        := by apply pnat.le_total ⦄
 
 notation 2 := (tag 2 dec_trivial : ℕ+)
 notation 3 := (tag 3 dec_trivial : ℕ+)
@@ -273,9 +275,6 @@ end
 protected theorem mul_le_mul_right (p q : ℕ+) : p ≤ p * q :=
 by rewrite pnat.mul_comm; apply pnat.mul_le_mul_left
 
-theorem pnat.lt_of_not_le {p q : ℕ+} : ¬ p ≤ q → q < p :=
-begin rewrite [pnat.le_def, pnat.lt_def], apply lt_of_not_ge end
-
 protected theorem inv_cancel_left (p : ℕ+) : rat_of_pnat p * p⁻¹ = (1 : ℚ) :=
 mul_one_div_cancel (ne.symm (ne_of_lt !rat_of_pnat_is_pos))
 
diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index 13f3bdf55..c2789a1d5 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -199,7 +199,7 @@ theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t)
       apply rat.le_trans,
       apply rat.add_le_add_left,
       apply add_le_add,
-      apply HNj (max j Nj) (pnat.max_right j Nj),
+      apply HNj (max j Nj) (le_max_right j Nj),
       apply Ht,
       have hsimp : ∀ m : ℕ+, n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹),
         from λm, calc
@@ -211,8 +211,8 @@ theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t)
       rewrite hsimp,
       have Hms : (max j Nj)⁻¹ + (max j Nj)⁻¹ ≤ j⁻¹ + j⁻¹, begin
         apply add_le_add,
-        apply inv_ge_of_le (pnat.max_left j Nj),
-        apply inv_ge_of_le (pnat.max_left j Nj),
+        apply inv_ge_of_le (le_max_left j Nj),
+        apply inv_ge_of_le (le_max_left j Nj),
       end,
      apply (calc
        n⁻¹ + n⁻¹ + j⁻¹ + ((max j Nj)⁻¹ + (max j Nj)⁻¹) ≤ n⁻¹ + n⁻¹ + j⁻¹ + (j⁻¹ + j⁻¹) :
@@ -303,30 +303,19 @@ theorem bdd_of_regular_strict {s : seq} (H : regular s) : ∃ b : ℚ, ∀ n : 
 definition K₂ (s t : seq) := max (K s) (K t)
 
 private theorem K₂_symm (s t : seq) : K₂ s t = K₂ t s :=
-  if H : K s < K t then
-    (have H1 : K₂ s t = K t, from pnat.max_eq_right H,
-     have H2 : K₂ t s = K t, from pnat.max_eq_left (pnat.not_lt_of_ge (pnat.le_of_lt H)),
-     by rewrite [H1, -H2])
-  else
-    (have H1 : K₂ s t = K s, from pnat.max_eq_left H,
-      if J : K t < K s then
-        (have H2 : K₂ t s = K s, from pnat.max_eq_right J, by rewrite [H1, -H2])
-      else
-        (have Heq : K t = K s, from
-          pnat.eq_of_le_of_ge (pnat.le_of_not_gt H) (pnat.le_of_not_gt J),
-        by rewrite [↑K₂, Heq]))
+!max.comm
 
 theorem canon_2_bound_left (s t : seq) (Hs : regular s) (n : ℕ+) :
         abs (s n) ≤ rat_of_pnat (K₂ s t) :=
   calc
     abs (s n) ≤ rat_of_pnat (K s) : canon_bound Hs n
-    ... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!pnat.max_left)
+    ... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!le_max_left)
 
 theorem canon_2_bound_right (s t : seq) (Ht : regular t) (n : ℕ+) :
         abs (t n) ≤ rat_of_pnat (K₂ s t) :=
   calc
     abs (t n) ≤ rat_of_pnat (K t) : canon_bound Ht n
-    ... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!pnat.max_right)
+    ... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!le_max_right)
 
 definition sadd (s t : seq) : seq := λ n, (s (2 * n)) + (t (2 * n))
 
@@ -710,12 +699,12 @@ theorem s_distrib {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular
     apply abs_add_le_abs_add_abs,
     apply add_le_add,
     apply HN1,
-    apply pnat.le_trans,
-    apply pnat.max_left N1 N2,
+    apply le.trans,
+    apply le_max_left N1 N2,
     apply Hn,
     apply HN2,
-    apply pnat.le_trans,
-    apply pnat.max_right N1 N2,
+    apply le.trans,
+    apply le_max_right N1 N2,
     apply Hn
   end
 
@@ -738,7 +727,7 @@ theorem mul_zero_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t) (Htz :
     have HN' : ∀ (n : ℕ+), N ≤ n → abs (t n) ≤ ε / Kq s,
       from λ n, (eq.subst (sub_zero (t n)) (HN n)),
     apply HN',
-    apply pnat.le_trans Hn,
+    apply le.trans Hn,
     apply pnat.mul_le_mul_left,
     apply abs_nonneg,
     apply le_of_lt (Kq_bound_pos Hs),
@@ -915,7 +904,7 @@ theorem zero_nequiv_one : ¬ zero ≡ one :=
       ... = abs 1 : abs_of_pos zero_lt_one
       ... ≤ 2⁻¹ : H,
     let H'' := ge_of_inv_le H',
-    apply absurd (one_lt_two) (pnat.not_lt_of_ge H'')
+    apply absurd (one_lt_two) (not_lt_of_ge H'')
   end
 
 ---------------------------------------------
diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean
index a7b92cee4..0beece400 100644
--- a/library/data/real/complete.lean
+++ b/library/data/real/complete.lean
@@ -56,7 +56,7 @@ theorem rat_approx_seq {s : seq} (H : regular s) :
     rewrite -sub_eq_add_neg,
     apply sub_le_sub_left,
     apply HN,
-    apply pnat.le_trans,
+    apply le.trans,
     apply Hp,
     rewrite -*pnat.mul_assoc,
     apply pnat.mul_le_mul_left,
@@ -289,11 +289,11 @@ theorem cauchy_with_rate_of_converges_to_with_rate {X : r_seq} {a : ℝ} {N : 
     krewrite pnat.add_halves,
   end
 
-private definition Nb (M : ℕ+ → ℕ+) := λ k, pnat.max (3 * k) (M (2 * k))
+private definition Nb (M : ℕ+ → ℕ+) := λ k, max (3 * k) (M (2 * k))
 
-private theorem Nb_spec_right (M : ℕ+ → ℕ+) (k : ℕ+) : M (2 * k) ≤ Nb M k := !pnat.max_right
+private theorem Nb_spec_right (M : ℕ+ → ℕ+) (k : ℕ+) : M (2 * k) ≤ Nb M k := !le_max_right
 
-private theorem Nb_spec_left (M : ℕ+ → ℕ+) (k : ℕ+) : 3 * k ≤ Nb M k := !pnat.max_left
+private theorem Nb_spec_left (M : ℕ+ → ℕ+) (k : ℕ+) : 3 * k ≤ Nb M k := !le_max_left
 
 section lim_seq
 parameter {X : r_seq}
@@ -318,7 +318,7 @@ private theorem lim_seq_reg_helper {m n : ℕ+} (Hmn : M (2 * n) ≤M (2 * m)) :
     rotate 1,
     apply Nb_spec_right,
     rotate 1,
-    apply pnat.le_trans,
+    apply le.trans,
     apply Hmn,
     apply Nb_spec_right,
     krewrite [-+of_rat_add],
@@ -341,7 +341,7 @@ theorem lim_seq_reg : rat_seq.regular lim_seq :=
     apply abs_add_three,
     cases em (M (2 * m) ≥ M (2 * n)) with [Hor1, Hor2],
     apply lim_seq_reg_helper Hor1,
-    let Hor2' := pnat.le_of_lt (pnat.lt_of_not_le Hor2),
+    let Hor2' := le_of_lt (lt_of_not_ge Hor2),
     krewrite [abs_sub (X (Nb M n)), abs_sub (X (Nb M m)), abs_sub,
              rat.add_comm, add_comm_three],
     apply lim_seq_reg_helper Hor2'
@@ -383,17 +383,17 @@ theorem converges_to_with_rate_of_cauchy_with_rate : converges_to_with_rate X li
     apply le.trans,
     apply add_le_add_three,
     apply Hc,
-    apply pnat.le_trans,
+    apply le.trans,
     rotate 1,
     apply Hn,
     rotate_right 1,
     apply Nb_spec_right,
     have HMk : M (2 * k) ≤ Nb M n, begin
-      apply pnat.le_trans,
+      apply le.trans,
       apply Nb_spec_right,
-      apply pnat.le_trans,
+      apply le.trans,
       apply Hn,
-      apply pnat.le_trans,
+      apply le.trans,
       apply pnat.mul_le_mul_left 3,
       apply Nb_spec_left
     end,
@@ -409,13 +409,13 @@ theorem converges_to_with_rate_of_cauchy_with_rate : converges_to_with_rate X li
     apply rat.le_refl,
     apply inv_ge_of_le,
     apply pnat_mul_le_mul_left',
-    apply pnat.le_trans,
+    apply le.trans,
     rotate 1,
     apply Hn,
     rotate_right 1,
     apply Nb_spec_left,
     apply inv_ge_of_le,
-    apply pnat.le_trans,
+    apply le.trans,
     rotate 1,
     apply Hn,
     rotate_right 1,
@@ -442,7 +442,7 @@ theorem archimedean_upper (x : ℝ) : ∃ z : ℤ, x ≤ of_int z :=
       apply rat_seq.s_le_of_le_pointwise (rat_seq.reg_seq.is_reg s),
       apply rat_seq.const_reg,
       intro n,
-      apply rat.le_trans,
+      apply le.trans,
       apply Hb,
       apply ubound_ge
     end,
@@ -814,7 +814,7 @@ private theorem under_seq_mono_helper (i k : ℕ) : under_seq i ≤ under_seq (i
       rewrite (if_pos Havg),
       apply Ha,
       rewrite [if_neg Havg, ↑avg_seq, ↑avg],
-      apply rat.le_trans,
+      apply le.trans,
       apply Ha,
       rewrite -(add_halves (under_seq (i + a))) at {1},
       apply add_le_add_right,
@@ -839,7 +839,7 @@ private theorem over_seq_mono_helper (i k : ℕ) : over_seq (i + k) ≤ over_seq
       rewrite [add_succ, over_succ],
       cases em (ub (avg_seq (i + a))) with [Havg, Havg],
       rewrite [if_pos Havg, ↑avg_seq, ↑avg],
-      apply rat.le_trans,
+      apply le.trans,
       rotate 1,
       apply Ha,
       rotate 1,
@@ -869,15 +869,15 @@ private theorem regular_lemma_helper {s : seq} {m n : ℕ+} (Hm : m ≤ n)
         abs (s m - s n) ≤ m⁻¹ + n⁻¹ :=
   begin
     cases H m n Hm with [T1under, T1over],
-    cases H m m (!pnat.le_refl) with [T2under, T2over],
-    apply rat.le_trans,
+    cases H m m (!le.refl) with [T2under, T2over],
+    apply le.trans,
     apply dist_bdd_within_interval,
     apply under_seq'_lt_over_seq'_single,
     rotate 1,
     repeat assumption,
-    apply rat.le_trans,
+    apply le.trans,
     apply width',
-    apply rat.le_trans,
+    apply le.trans,
     apply rat_power_two_inv_ge,
     apply le_add_of_nonneg_right,
     apply rat.le_of_lt (!pnat.inv_pos)
@@ -890,7 +890,7 @@ private theorem regular_lemma (s : seq) (H : ∀ n i : ℕ+, i ≥ n → under_s
     intros,
     cases em (m ≤ n) with [Hm, Hn],
     apply regular_lemma_helper Hm H,
-    note T := regular_lemma_helper (pnat.le_of_lt (pnat.lt_of_not_le Hn)) H,
+    note T := regular_lemma_helper (le_of_lt (lt_of_not_ge Hn)) H,
     rewrite [abs_sub at T, {n⁻¹ + _}add.comm at T],
     exact T
   end
@@ -954,11 +954,11 @@ private theorem under_lowest_bound : ∀ y : ℝ, ub y → sup_under ≤ y :=
 private theorem under_over_equiv : p_under_seq ≡ p_over_seq :=
   begin
     intros,
-    apply rat.le_trans,
+    apply le.trans,
     have H : p_under_seq n < p_over_seq n, from !under_seq_lt_over_seq,
     rewrite [abs_of_neg (iff.mpr !sub_neg_iff_lt H), neg_sub],
     apply width',
-    apply rat.le_trans,
+    apply le.trans,
     apply rat_power_two_inv_ge,
     apply le_add_of_nonneg_left,
     apply rat.le_of_lt !pnat.inv_pos
diff --git a/library/data/real/division.lean b/library/data/real/division.lean
index 5d1acfb7c..cceeadbd6 100644
--- a/library/data/real/division.lean
+++ b/library/data/real/division.lean
@@ -122,7 +122,7 @@ private theorem s_inv_of_sep_gt_p {s : seq} (Hs : regular s) (Hsep : sep s zero)
   begin
     apply eq.trans,
     apply dif_pos Hsep,
-    apply dif_neg (pnat.not_lt_of_ge Hn)
+    apply dif_neg (not_lt_of_ge Hn)
   end
 
 private theorem s_inv_of_pos_lt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
@@ -144,7 +144,7 @@ private theorem le_ps {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+)
     end)
   else
     (begin
-      rewrite [(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hn)), abs_one_div],
+      rewrite [(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hn)), abs_one_div],
       apply div_le_pnat,
       apply ps_spec,
       rewrite pnat.mul_assoc,
@@ -194,7 +194,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
         rewrite [sub_self, abs_zero],
         apply add_invs_nonneg,
        rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt),
-                (s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hnlt))],
+                (s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt))],
        rewrite [(!div_sub_div Hsp Hspn), div_eq_mul_one_div, *abs_mul, *mul_one, *one_mul],
        apply le.trans,
        apply mul_le_mul,
@@ -203,7 +203,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
        apply mul_le_mul,
        rewrite -(s_inv_of_sep_lt_p Hs Hsep Hmlt),
        apply le_ps Hs Hsep,
-       rewrite  -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hnlt)),
+       rewrite  -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt)),
        apply le_ps Hs Hsep,
        apply abs_nonneg,
        apply le_of_lt !rat_of_pnat_is_pos,
@@ -212,18 +212,18 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
        rewrite [right_distrib, *pnat_cancel', add.comm],
        apply add_le_add_right,
        apply inv_ge_of_le,
-       apply pnat.le_of_lt,
+       apply le_of_lt,
        apply Hmlt,
       cases em (n < ps Hs Hsep) with [Hnlt, Hnlt],
         rewrite [(s_inv_of_sep_lt_p Hs Hsep Hnlt),
-                 (s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt))],
+                 (s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt))],
         rewrite [(!div_sub_div Hspm Hsp), div_eq_mul_one_div, *abs_mul, *mul_one, *one_mul],
         apply le.trans,
         apply mul_le_mul,
         apply Hs,
         rewrite [-(mul_one 1), -(!field.div_mul_div Hspm Hsp), abs_mul],
         apply mul_le_mul,
-        rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt)),
+        rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt)),
         apply le_ps Hs Hsep,
         rewrite -(s_inv_of_sep_lt_p Hs Hsep Hnlt),
         apply le_ps Hs Hsep,
@@ -234,19 +234,19 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
         rewrite [right_distrib, *pnat_cancel', add.comm],
         apply rat.add_le_add_left,
         apply inv_ge_of_le,
-        apply pnat.le_of_lt,
+        apply le_of_lt,
         apply Hnlt,
-      rewrite [(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hnlt)),
-              (s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt))],
+      rewrite [(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt)),
+              (s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt))],
       rewrite [(!div_sub_div Hspm Hspn), div_eq_mul_one_div, abs_mul, *one_mul, *mul_one],
       apply le.trans,
       apply mul_le_mul,
       apply Hs,
       rewrite [-(mul_one 1), -(!field.div_mul_div Hspm Hspn), abs_mul],
       apply mul_le_mul,
-      rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt)),
+      rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt)),
       apply le_ps Hs Hsep,
-      rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hnlt)),
+      rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt)),
       apply le_ps Hs Hsep,
       apply abs_nonneg,
       apply le_of_lt !rat_of_pnat_is_pos,
@@ -262,13 +262,13 @@ theorem s_inv_ne_zero {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+)
       rewrite (s_inv_of_sep_gt_p Hs Hsep H),
       apply one_div_ne_zero,
       apply s_ne_zero_of_ge_p,
-      apply pnat.le_trans,
+      apply le.trans,
       apply H,
       apply pnat.mul_le_mul_left
     end)
   else
     (begin
-      rewrite (s_inv_of_sep_lt_p Hs Hsep (pnat.lt_of_not_le H)),
+      rewrite (s_inv_of_sep_lt_p Hs Hsep (lt_of_not_ge H)),
       apply one_div_ne_zero,
       apply s_ne_zero_of_ge_p,
       apply pnat.mul_le_mul_left
@@ -292,10 +292,10 @@ protected theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) :
     apply Rsi,
     apply abs_nonneg,
     have Hp : (K₂ s (s_inv Hs)) * 2 * n ≥ ps Hs Hsep, begin
-      apply pnat.le_trans,
-      apply pnat.max_left,
+      apply le.trans,
+      apply le_max_left,
       rotate 1,
-      apply pnat.le_trans,
+      apply le.trans,
       apply Hn,
       apply pnat.mul_le_mul_left
     end,
@@ -315,17 +315,17 @@ protected theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) :
     apply add_le_add,
     apply inv_ge_of_le,
     apply pnat_mul_le_mul_left',
-    apply pnat.le_trans,
+    apply le.trans,
     rotate 1,
     apply Hn,
     rotate_right 1,
-    apply pnat.max_right,
+    apply le_max_right,
     apply inv_ge_of_le,
     apply pnat_mul_le_mul_left',
-    apply pnat.le_trans,
-    apply pnat.max_right,
+    apply le.trans,
+    apply le_max_right,
     rotate 1,
-    apply pnat.le_trans,
+    apply le.trans,
     apply Hn,
     apply pnat.mul_le_mul_right
    end
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index 25ada2763..b8ae1553d 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -58,7 +58,7 @@ theorem pos_of_bdd_away {s : seq} (H : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (
     apply lt_of_lt_of_le,
     apply inv_add_lt_left,
     apply HN,
-    apply pnat.le_of_lt,
+    apply le_of_lt,
     apply lt_add_left
   end
 
@@ -94,11 +94,11 @@ theorem nonneg_of_bdd_within {s : seq} (Hs : regular s)
     rotate 1,
     apply add_le_add,
     rotate 1,
-    apply HN (max (pceil ((2)/ε)) N) !pnat.max_right,
+    apply HN (max (pceil ((2)/ε)) N) !le_max_right,
     rotate_right 1,
     apply neg_le_neg,
     apply inv_ge_of_le,
-    apply pnat.max_left,
+    apply le_max_left,
     rewrite -neg_add,
     apply neg_le_neg,
     apply le.trans,
@@ -146,17 +146,17 @@ theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (He
     rotate 1,
     apply sub_le_sub_right,
     apply HNs,
-    apply pnat.le_trans,
+    apply le.trans,
     rotate 1,
     apply Hm,
     rotate_right 1,
-    apply pnat.max_left,
+    apply le_max_left,
     have Hms : m⁻¹ ≤ (2 * 2 * n)⁻¹, begin
          apply inv_ge_of_le,
-         apply pnat.le_trans,
+         apply le.trans,
          rotate 1,
          apply Hm;
-         apply pnat.max_right
+         apply le_max_right
       end,
     have Hms' : m⁻¹ + m⁻¹ ≤ (2 * 2 * n)⁻¹ + (2 * 2 * n)⁻¹, from add_le_add Hms Hms,
     apply le.trans,
@@ -492,13 +492,13 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
     rotate 1,
     apply mul_le_mul,
     apply HNs,
-    apply pnat.le_trans,
-    apply pnat.max_left Ns Nt,
+    apply le.trans,
+    apply le_max_left Ns Nt,
     rewrite -pnat.mul_assoc,
     apply pnat.mul_le_mul_left,
     apply HNt,
-    apply pnat.le_trans,
-    apply pnat.max_right Ns Nt,
+    apply le.trans,
+    apply le_max_right Ns Nt,
     rewrite -pnat.mul_assoc,
     apply pnat.mul_le_mul_left,
     apply rat.le_of_lt,
@@ -506,8 +506,8 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
     apply rat.le_trans,
     rotate 1,
     apply HNs,
-    apply pnat.le_trans,
-    apply pnat.max_left Ns Nt,
+    apply le.trans,
+    apply le_max_left Ns Nt,
     rewrite -pnat.mul_assoc,
     apply pnat.mul_le_mul_left,
     rewrite pnat.inv_mul_eq_mul_inv,
@@ -517,11 +517,11 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
     apply inv_lt_one_of_gt,
     apply dec_trivial,
     apply inv_ge_of_le,
-    apply pnat.max_left,
+    apply le_max_left,
     apply pnat.inv_pos,
     apply rat.le_of_lt zero_lt_one,
     apply inv_ge_of_le,
-    apply pnat.max_right,
+    apply le_max_right,
     apply pnat.inv_pos,
     repeat (apply le_of_lt; apply pnat.inv_pos)
   end
@@ -789,22 +789,22 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
     rotate 1,
     apply add_le_add,
     apply HNt,
-    apply pnat.le_trans,
+    apply le.trans,
     apply pnat.mul_le_mul_left 2,
-    apply pnat.le_trans,
+    apply le.trans,
     rotate 1,
     apply Hn,
     rotate_right 1,
-    apply pnat.max_left,
+    apply le_max_left,
     apply HNu,
-    apply pnat.le_trans,
+    apply le.trans,
     rotate 1,
     apply Hn,
     rotate_right 1,
-    apply pnat.max_right,
+    apply le_max_right,
     rewrite [-pnat.add_halves Nt, -sub_eq_add_neg, add_sub_cancel],
     apply inv_ge_of_le,
-    apply pnat.max_left
+    apply le_max_left
   end
 
 theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
@@ -827,22 +827,22 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
     rotate 1,
     apply add_le_add,
     apply HNt,
-    apply pnat.le_trans,
+    apply le.trans,
     rotate 1,
     apply Hn,
     rotate_right 1,
-    apply pnat.max_right,
+    apply le_max_right,
     apply HNu,
-    apply pnat.le_trans,
+    apply le.trans,
     apply pnat.mul_le_mul_left 2,
-    apply pnat.le_trans,
+    apply le.trans,
     rotate 1,
     apply Hn,
     rotate_right 1,
-    apply pnat.max_left,
+    apply le_max_left,
     rewrite [-pnat.add_halves Nu, neg_add_cancel_left],
     apply inv_ge_of_le,
-    apply pnat.max_left
+    apply le_max_left
   end
 
 theorem le_of_le_reprs {s t : seq} (Hs : regular s) (Ht : regular t)
@@ -884,7 +884,7 @@ theorem nat_inv_lt_rat {a : ℚ} (H : a > 0) : ∃ n : ℕ+, n⁻¹ < a :=
     apply div_two_lt_of_pos H,
     rewrite -(one_div_one_div (a / (1 + 1))),
     apply pceil_helper,
-    apply pnat.le_refl,
+    apply le.refl,
     apply one_div_pos_of_pos,
     apply div_pos_of_pos_of_pos H dec_trivial
   end