refactor(library/algebra/order.lean,library/{data,algebra}/*): use better names for order theorems

library/algebra/order.lean

@@ -95,7 +95,7 @@ section
   theorem lt.asymm {a b : A} (H : a < b) : ¬ b < a :=
   assume H1 : b < a, lt.irrefl _ (lt.trans H H1)
 
-  theorem not_lt_of_lt {a b : A} (H : a < b) : ¬ b < a := !lt.asymm H    -- alternate syntax
+  theorem not_lt_of_gt {a b : A} (H : a > b) : ¬ a < b := !lt.asymm H    -- alternate syntax
 end
 
 /- well-founded orders -/
@@ -178,12 +178,12 @@ section
 
   theorem gt_of_ge_of_gt [trans] (H1 : a ≥ b) (H2 : b > c) : a > c := lt_of_lt_of_le H2 H1
 
-  theorem not_le_of_lt (H : a < b) : ¬ b ≤ a :=
-  assume H1 : b ≤ a,
+  theorem not_le_of_gt (H : a > b) : ¬ a ≤ b :=
+  assume H1 : a ≤ b,
   lt.irrefl _ (lt_of_lt_of_le H H1)
 
-  theorem not_lt_of_le (H : a ≤ b) : ¬ b < a :=
-  assume H1 : b < a,
+  theorem not_lt_of_ge (H : a ≥ b) : ¬ a < b :=
+  assume H1 : a < b,
   lt.irrefl _ (lt_of_le_of_lt H H1)
 end
 
@@ -274,10 +274,10 @@ section
      : linear_order_pair A :=
   ⦃ linear_order_pair, s ⦄
 
-  theorem le_of_not_lt {a b : A} (H : ¬ a < b) : b ≤ a :=
+  theorem le_of_not_gt {a b : A} (H : ¬ a > b) : a ≤ b :=
   lt.by_cases (assume H', absurd H' H) (assume H', H' ▸ !le.refl) (assume H', le_of_lt H')
 
-  theorem lt_of_not_le {a b : A} (H : ¬ a ≤ b) : b < a :=
+  theorem lt_of_not_ge {a b : A} (H : ¬ a ≥ b) : a < b :=
   lt.by_cases
     (assume H', absurd (le_of_lt H') H)
     (assume H', absurd (H' ▸ !le.refl) H)
@@ -312,10 +312,10 @@ section
   by_cases
     (assume H : a < b, inl (le_of_lt H))
     (assume H : ¬ a < b,
-      have H1 : b ≤ a, from le_of_not_lt H,
+      have H1 : b ≤ a, from le_of_not_gt H,
       by_cases
-        (assume H2 : b < a, inr (not_le_of_lt H2))
-        (assume H2 : ¬ b < a, inl (le_of_not_lt H2)))
+        (assume H2 : b < a, inr (not_le_of_gt H2))
+        (assume H2 : ¬ b < a, inl (le_of_not_gt H2)))
 
   definition has_decidable_eq [instance] : decidable (a = b) :=
   by_cases

library/algebra/ordered_field.lean

@@ -275,7 +275,7 @@ section discrete_linear_ordered_field
       decidable.by_cases
       (assume H' : y < x, decidable.inr (ne.symm (ne_of_lt H')))
       (assume H' : ¬ y < x,
-        decidable.inl (le.antisymm (le_of_not_lt H') (le_of_not_lt H))))
+        decidable.inl (le.antisymm (le_of_not_gt H') (le_of_not_gt H))))
 
   definition discrete_linear_ordered_field.to_discrete_field [instance] [reducible] [coercion]
     [s : discrete_linear_ordered_field A] :  discrete_field A :=
@@ -343,24 +343,24 @@ section discrete_linear_ordered_field
 
 
   theorem div_lt_div_of_lt (Ha : 0 < a) (H : a < b) : 1 / b < 1 / a :=
-    lt_of_not_le
+    lt_of_not_ge
       (assume H',
-      absurd H (not_lt_of_le (le_of_div_le Ha H')))
+      absurd H (not_lt_of_ge (le_of_div_le Ha H')))
 
   theorem div_le_div_of_le (Ha : 0 < a) (H : a ≤ b) : 1 / b ≤ 1 / a :=
-    le_of_not_lt
+    le_of_not_gt
       (assume H',
-      absurd H (not_le_of_lt (lt_of_div_lt Ha H')))
+      absurd H (not_le_of_gt (lt_of_div_lt Ha H')))
 
   theorem div_lt_div_of_lt_neg (Hb : b < 0) (H : a < b) : 1 / b < 1 / a :=
-    lt_of_not_le
+    lt_of_not_ge
       (assume H',
-      absurd H (not_lt_of_le (le_of_div_le_neg Hb H')))
+      absurd H (not_lt_of_ge (le_of_div_le_neg Hb H')))
 
   theorem div_le_div_of_le_neg (Hb : b < 0) (H : a ≤ b) : 1 / b ≤ 1 / a :=
-    le_of_not_lt
+    le_of_not_gt
       (assume H',
-      absurd H (not_le_of_lt (lt_of_div_lt_neg Hb H')))
+      absurd H (not_le_of_gt (lt_of_div_lt_neg Hb H')))
 
 
   theorem one_lt_div (H1 : 0 < a) (H2 : a < 1) : 1 < 1 / a :=

library/algebra/ordered_group.lean

@@ -420,7 +420,7 @@ section
 
   theorem abs_of_pos (H : a > 0) : abs a = a := if_pos (le_of_lt H)
 
-  theorem abs_of_neg (H : a < 0) : abs a = -a := if_neg (not_le_of_lt H)
+  theorem abs_of_neg (H : a < 0) : abs a = -a := if_neg (not_le_of_gt H)
 
   theorem abs_zero : abs 0 = (0:A) := abs_of_nonneg (le.refl _)
 
@@ -496,7 +496,7 @@ section
                 ... = abs a + b         : by rewrite (abs_of_nonneg H2)
                 ... = abs a + abs b     : by rewrite (abs_of_nonneg H3))
       (assume H3 : ¬ b ≥ 0,
-        assert H4 : b ≤ 0, from le_of_lt (lt_of_not_le H3),
+        assert H4 : b ≤ 0, from le_of_lt (lt_of_not_ge H3),
         calc
           abs (a + b) = a + b     : by rewrite (abs_of_nonneg H1)
               ... = abs a + b     : by rewrite (abs_of_nonneg H2)
@@ -510,8 +510,8 @@ section
         have H3 : ¬ a < 0, from
           assume H4 : a < 0,
           have H5 : a + b < 0, from !add_zero ▸ add_lt_add_of_lt_of_le H4 H2,
-          not_lt_of_le H1 H5,
-        aux1 H1 (le_of_not_lt H3))
+          not_lt_of_ge H1 H5,
+        aux1 H1 (le_of_not_gt H3))
       (assume H2 : 0 ≤ b,
         begin
           have H3 : abs (b + a) ≤ abs b + abs a,

library/algebra/ordered_ring.lean

@@ -110,40 +110,40 @@ section
   include s
 
   theorem lt_of_mul_lt_mul_left (H : c * a < c * b) (Hc : c ≥ 0) : a < b :=
-  lt_of_not_le
+  lt_of_not_ge
     (assume H1 : b ≤ a,
       have H2 : c * b ≤ c * a, from mul_le_mul_of_nonneg_left H1 Hc,
-      not_lt_of_le H2 H)
+      not_lt_of_ge H2 H)
 
   theorem lt_of_mul_lt_mul_right (H : a * c < b * c) (Hc : c ≥ 0) : a < b :=
-  lt_of_not_le
+  lt_of_not_ge
     (assume H1 : b ≤ a,
       have H2 : b * c ≤ a * c, from mul_le_mul_of_nonneg_right H1 Hc,
-      not_lt_of_le H2 H)
+      not_lt_of_ge H2 H)
 
   theorem le_of_mul_le_mul_left (H : c * a ≤ c * b) (Hc : c > 0) : a ≤ b :=
-  le_of_not_lt
+  le_of_not_gt
     (assume H1 : b < a,
       have H2 : c * b < c * a, from mul_lt_mul_of_pos_left H1 Hc,
-      not_le_of_lt H2 H)
+      not_le_of_gt H2 H)
 
   theorem le_of_mul_le_mul_right (H : a * c ≤ b * c) (Hc : c > 0) : a ≤ b :=
-  le_of_not_lt
+  le_of_not_gt
     (assume H1 : b < a,
       have H2 : b * c < a * c, from mul_lt_mul_of_pos_right H1 Hc,
-      not_le_of_lt H2 H)
+      not_le_of_gt H2 H)
 
   theorem pos_of_mul_pos_left (H : 0 < a * b) (H1 : 0 ≤ a) : 0 < b :=
-  lt_of_not_le
+  lt_of_not_ge
     (assume H2 : b ≤ 0,
       have H3 : a * b ≤ 0, from mul_nonpos_of_nonneg_of_nonpos H1 H2,
-      not_lt_of_le H3 H)
+      not_lt_of_ge H3 H)
 
   theorem pos_of_mul_pos_right (H : 0 < a * b) (H1 : 0 ≤ b) : 0 < a :=
-  lt_of_not_le
+  lt_of_not_ge
     (assume H2 : a ≤ 0,
       have H3 : a * b ≤ 0, from mul_nonpos_of_nonpos_of_nonneg H2 H1,
-      not_lt_of_le H3 H)
+      not_lt_of_ge H3 H)
 end
 
 structure ordered_ring [class] (A : Type) extends ring A, ordered_comm_group A, zero_ne_one_class A :=

library/data/int/order.lean

@@ -331,7 +331,7 @@ sign_of_pos (of_nat_pos !nat.succ_pos)
 
 theorem exists_eq_neg_succ_of_nat {a : ℤ} : a < 0 → ∃m : ℕ, a = -[m +1] :=
 int.cases_on a
-  (take m H, absurd (of_nat_nonneg m) (not_le_of_lt H))
+  (take m H, absurd (of_nat_nonneg m : 0 ≤ m) (not_le_of_gt H))
   (take m H, exists.intro m rfl)
 
 end int

library/data/nat/div.lean

@@ -32,7 +32,7 @@ theorem div_zero (a : ℕ) : a div 0 = 0 :=
 divide_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0))
 
 theorem div_eq_zero_of_lt {a b : ℕ} (h : a < b) : a div b = 0 :=
-divide_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_lt h))
+divide_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_gt h))
 
 theorem zero_div (b : ℕ) : 0 div b = 0 :=
 divide_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l r) (lt.irrefl 0)))
@@ -87,7 +87,7 @@ theorem mod_zero (a : ℕ) : a mod 0 = a :=
 modulo_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0))
 
 theorem mod_eq_of_lt {a b : ℕ} (h : a < b) : a mod b = a :=
-modulo_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_lt h))
+modulo_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_gt h))
 
 theorem zero_mod (b : ℕ) : 0 mod b = 0 :=
 modulo_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l r) (lt.irrefl 0)))
@@ -139,7 +139,7 @@ nat.case_strong_induction_on x
           have H2 : succ x mod y = succ x, from mod_eq_of_lt H1,
           show succ x mod y < y, from H2⁻¹ ▸ H1)
         (assume H1 : ¬ succ x < y,
-          have H2 : y ≤ succ x, from le_of_not_lt H1,
+          have H2 : y ≤ succ x, from le_of_not_gt H1,
           have H3 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2,
           have H4 : succ x - y < succ x, from sub_lt !succ_pos H,
           have H5 : succ x - y ≤ x, from le_of_lt_succ H4,
@@ -169,7 +169,7 @@ by_cases_zero_pos y
                 have H3 : succ x mod y = succ x, from mod_eq_of_lt H1,
                 by simp)
               (assume H1 : ¬ succ x < y,
-                have H2 : y ≤ succ x, from le_of_not_lt H1,
+                have H2 : y ≤ succ x, from le_of_not_gt H1,
                 have H3 : succ x div y = succ ((succ x - y) div y), from div_eq_succ_sub_div H H2,
                 have H4 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2,
                 have H5 : succ x - y < succ x, from sub_lt !succ_pos H,
@@ -392,7 +392,7 @@ by_cases
     have H4 : n1 = n1 - n2 + n2, from (sub_add_cancel H3)⁻¹,
     show m ∣ n1 - n2, from dvd_of_dvd_add_right (H4 ▸ H1) H2)
   (assume H3 : ¬ (n1 ≥ n2),
-    have H4 : n1 - n2 = 0, from sub_eq_zero_of_le (le_of_lt (lt_of_not_le H3)),
+    have H4 : n1 - n2 = 0, from sub_eq_zero_of_le (le_of_lt (lt_of_not_ge H3)),
     show m ∣ n1 - n2, from H4⁻¹ ▸ dvd_zero _)
 
 theorem dvd.antisymm {m n : ℕ} : m ∣ n → n ∣ m → m = n :=

library/data/nat/order.lean

@@ -279,9 +279,9 @@ nat.cases_on n
     !pred_succ⁻¹ ▸ succ_le_of_le_pred H)
 
 theorem lt_of_pred_lt_pred {n m : ℕ} (H : pred n < pred m) : n < m :=
-lt_of_not_le
+lt_of_not_ge
   (take H1 : m ≤ n,
-    not_lt_of_le (pred_le_pred_of_le H1) H)
+    not_lt_of_ge (pred_le_pred_of_le H1) H)
 
 theorem le_or_eq_succ_of_le_succ {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m :=
 or_of_or_of_imp_left (succ_le_or_eq_of_le H)
@@ -407,7 +407,7 @@ or.elim (le_or_gt n 1)
   (assume H5 : n > 1,
     have H6 : n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt H5) (succ_le_of_lt H4),
     have H7 : 1 ≥ 2, from !mul_one ▸ H ▸ H6,
-    absurd !lt_succ_self (not_lt_of_le H7))
+    absurd !lt_succ_self (not_lt_of_ge H7))
 
 theorem eq_one_of_mul_eq_one_left {n m : ℕ} (H : n * m = 1) : m = 1 :=
 eq_one_of_mul_eq_one_right (!mul.comm ▸ H)

library/data/nat/pairing.lean

@@ -27,7 +27,7 @@ by_cases
       rewrite [if_pos h₁, add_sub_of_le (sqrt_lower n)]
     end)
   (λ h₂ : ¬ n - s*s < s,
-    have   g₁ : s ≤ n - s*s,             from le_of_not_lt h₂,
+    have   g₁ : s ≤ n - s*s,             from le_of_not_gt h₂,
     assert g₂ : s + s*s ≤ n - s*s + s*s, from add_le_add_right g₁ (s*s),
     assert g₃ : s*s + s ≤ n,             by rewrite [sub_add_cancel (sqrt_lower n) at g₂, add.comm at g₂]; exact g₂,
     have l₁   : n ≤ s*s + s + s,         from sqrt_upper n,
@@ -38,7 +38,7 @@ by_cases
     have l₃   : n - s*s - s ≤ s,         from calc
         n - s*s - s ≤ (s + s) - s        : sub_le_sub_right l₂ s
                 ... = s                  : by rewrite add_sub_cancel_left,
-    assert l₄ : ¬ s < n - s*s - s,       from not_lt_of_le l₃,
+    assert l₄ : ¬ s < n - s*s - s,       from not_lt_of_ge l₃,
     begin
       esimp [unpair],
       rewrite [if_neg h₂], esimp,
@@ -59,10 +59,10 @@ by_cases
     rewrite [sqrt_offset_eq aux₁, add_sub_cancel_left, if_pos h]
   end)
  (λ h : ¬ a < b,
-  have h₁ : b ≤ a, from le_of_not_lt h,
+  have h₁ : b ≤ a, from le_of_not_gt h,
   assert aux₁ : a + b ≤ a + a, from add_le_add_left h₁ a,
   have   aux₂ : a + b ≥ a,     from !le_add_right,
-  assert aux₃ : ¬ a + b < a,   from not_lt_of_le aux₂,
+  assert aux₃ : ¬ a + b < a,   from not_lt_of_ge aux₂,
   begin
     esimp [mkpair],
     rewrite [if_neg h],

library/data/nat/sqrt.lean

@@ -46,7 +46,7 @@ theorem sqrt_aux_upper : ∀ {s n : nat}, n ≤ s*s + s + s → n ≤ sqrt_aux s
   (λ h₁ : (succ s)*(succ s) ≤ n,
     by rewrite [sqrt_aux_succ_of_pos h₁]; exact h)
   (λ h₂ : ¬ (succ s)*(succ s) ≤ n,
-    assert h₃ : n < (succ s) * (succ s), from lt_of_not_le h₂,
+    assert h₃ : n < (succ s) * (succ s), from lt_of_not_ge h₂,
     assert h₄ : n ≤ s * s + s + s, by rewrite [succ_mul_succ_eq at h₃]; exact h₃,
     by rewrite [sqrt_aux_succ_of_neg h₂]; exact (sqrt_aux_upper h₄))
 
@@ -75,7 +75,7 @@ theorem sqrt_aux_offset_eq {n k : nat} (h₁ : k ≤ n + n) : ∀ {s}, s ≥ n
        assume g : succ s > succ n,
          have g₁ : (succ s)*(succ s) > (succ n)*(succ n), from mul_lt_mul_of_le_of_le g g,
          absurd (lt.trans g₁ l₄) !lt.irrefl,
-     have sslesn  : succ s ≤ succ n, from le_of_not_lt ng,
+     have sslesn  : succ s ≤ succ n, from le_of_not_gt ng,
      have ssnesn  : succ s ≠ succ n, from
        assume sseqsn : succ s = succ n,
          by rewrite [sseqsn at l₄]; exact (absurd l₄ !lt.irrefl),

library/data/nat/sub.lean

@@ -292,22 +292,22 @@ have H2 : 0 + m < n - m + m, from (zero_add m)⁻¹ ▸ H1 ▸ H,
 !lt_of_add_lt_add_right H2
 
 theorem lt_of_sub_pos {m n : ℕ} (H : n - m > 0) : m < n :=
-lt_of_not_le
+lt_of_not_ge
   (take H1 : m ≥ n,
     have H2 : n - m = 0, from sub_eq_zero_of_le H1,
     !lt.irrefl (H2 ▸ H))
 
 theorem lt_of_sub_lt_sub_right {n m k : ℕ} (H : n - k < m - k) : n < m :=
-lt_of_not_le
+lt_of_not_ge
   (assume H1 : m ≤ n,
     have H2 : m - k ≤ n - k, from sub_le_sub_right H1 _,
-    not_le_of_lt H H2)
+    not_le_of_gt H H2)
 
 theorem lt_of_sub_lt_sub_left {n m k : ℕ} (H : n - m < n - k) : k < m :=
-lt_of_not_le
+lt_of_not_ge
   (assume H1 : m ≤ k,
     have H2 : n - k ≤ n - m, from sub_le_sub_left H1 _,
-    not_le_of_lt H H2)
+    not_le_of_gt H H2)
 
 theorem sub_lt_sub_add_sub (n m k : ℕ) : n - k ≤ (n - m) + (m - k) :=
 sub.cases