feat(algebra/ordered...): Two tiny lemmas (leanprover-community#1522)

* feat(algebra/ordered...): Two tiny lemmas

* style(src/algebra/ordered_field)

Co-Authored-By: Reid Barton <rwbarton@gmail.com>

src/algebra/floor.lean

@@ -254,8 +254,11 @@ begin
   refl
 end
 
-theorem nat_ceil_lt_add_one {a : α} (a_nonneg : 0 ≤ a) [decidable (↑(nat_ceil a) < a + 1)] :
-  ↑(nat_ceil a) < a + 1 :=
+theorem nat_ceil_lt_add_one {a : α} (a_nonneg : 0 ≤ a) [decidable ((nat_ceil a : α) < a + 1)] :
+  (nat_ceil a : α) < a + 1 :=
 lt_nat_ceil.1 $ by rw (
   show nat_ceil (a + 1) = nat_ceil a + 1, by exact_mod_cast (nat_ceil_add_nat a_nonneg 1));
   apply nat.lt_succ_self
+
+lemma lt_of_nat_ceil_lt {x : α} {n : ℕ} (h : nat_ceil x < n) : x < n :=
+lt_of_le_of_lt (le_nat_ceil x) (by exact_mod_cast h)

src/algebra/ordered_field.lean

@@ -50,7 +50,7 @@ lemma div_le_iff_of_neg (hc : c < 0) : b / c ≤ a ↔ a * c ≤ b :=
 ⟨mul_le_of_div_le_of_neg hc, div_le_of_mul_le_of_neg hc⟩
 
 lemma le_div_iff_of_neg (hc : c < 0) : a ≤ b / c ↔ b ≤ a * c :=
-by rw [← neg_neg c, mul_neg_eq_neg_mul_symm, div_neg _ (ne_of_gt (neg_pos.2 hc)), le_neg, 
+by rw [← neg_neg c, mul_neg_eq_neg_mul_symm, div_neg _ (ne_of_gt (neg_pos.2 hc)), le_neg,
     div_le_iff (neg_pos.2 hc), neg_mul_eq_neg_mul_symm]
 
 lemma div_lt_iff (hc : 0 < c) : b / c < a ↔ b < a * c :=
@@ -81,6 +81,9 @@ lt_iff_lt_of_le_iff_le (inv_le_inv hb ha)
 lemma inv_lt (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b ↔ b⁻¹ < a :=
 lt_iff_lt_of_le_iff_le (le_inv hb ha)
 
+lemma one_div_lt (ha : 0 < a) (hb : 0 < b) : 1 / a < b ↔ 1 / b < a :=
+(one_div_eq_inv a).symm ▸ (one_div_eq_inv b).symm ▸ inv_lt ha hb
+
 lemma lt_inv (ha : 0 < a) (hb : 0 < b) : a < b⁻¹ ↔ b < a⁻¹ :=
 lt_iff_lt_of_le_iff_le (inv_le hb ha)